diff options
author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2017-09-22 19:50:52 +0200 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2017-09-22 19:50:52 +0200 |
commit | a36b3b755e25b8c5d61b9e069114858d9b768f04 (patch) | |
tree | 3ffd8bcb28a88ae4ff51989aed37b0ad2cb676b2 /cfrontend | |
parent | 0f210f622a4609811959f4450f770c61f5eb6532 (diff) | |
download | compcert-a36b3b755e25b8c5d61b9e069114858d9b768f04.tar.gz compcert-a36b3b755e25b8c5d61b9e069114858d9b768f04.zip |
Remove coq warnings (#28)
Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
Diffstat (limited to 'cfrontend')
-rw-r--r-- | cfrontend/Cexec.v | 2 | ||||
-rw-r--r-- | cfrontend/Cminorgen.v | 2 | ||||
-rw-r--r-- | cfrontend/Cminorgenproof.v | 16 | ||||
-rw-r--r-- | cfrontend/Ctypes.v | 56 | ||||
-rw-r--r-- | cfrontend/Initializers.v | 2 | ||||
-rw-r--r-- | cfrontend/Initializersproof.v | 10 | ||||
-rw-r--r-- | cfrontend/SimplExpr.v | 2 | ||||
-rw-r--r-- | cfrontend/SimplLocalsproof.v | 10 |
8 files changed, 50 insertions, 50 deletions
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index a9ffcd3d..15818317 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -1769,7 +1769,7 @@ Lemma not_stuckred_imm_safe: Proof. intros. generalize (step_expr_sound a k m). intros [A B]. destruct (step_expr k a m) as [|[C rd] res] eqn:?. - specialize (B (refl_equal _)). destruct k. + specialize (B (eq_refl _)). destruct k. destruct a; simpl in B; try congruence. constructor. destruct a; simpl in B; try congruence. constructor. assert (NOTSTUCK: rd <> Stuckred). diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index 5017fc8e..45c21f96 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -226,7 +226,7 @@ Definition assign_variable let (id, sz) := id_sz in let (cenv, stacksize) := cenv_stacksize in let ofs := align stacksize (block_alignment sz) in - (PTree.set id ofs cenv, ofs + Zmax 0 sz). + (PTree.set id ofs cenv, ofs + Z.max 0 sz). Definition assign_variables (cenv_stacksize: compilenv * Z) (vars: list (ident * Z)) : compilenv * Z := List.fold_left assign_variable vars cenv_stacksize. diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index a6d58f17..ffafc5d2 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -96,7 +96,7 @@ Proof. intros m1 FR1 FRL. transitivity (Mem.load chunk m1 b ofs). eapply IHfbl; eauto. intros. eapply H. eauto with coqlib. - eapply Mem.load_free; eauto. left. apply sym_not_equal. eapply H. auto with coqlib. + eapply Mem.load_free; eauto. left. apply not_eq_sym. eapply H. auto with coqlib. Qed. Lemma perm_freelist: @@ -775,7 +775,7 @@ Definition cenv_compat (cenv: compilenv) (vars: list (ident * Z)) (tsz: Z) : Pro PTree.get id cenv = Some ofs /\ Mem.inj_offset_aligned ofs sz /\ 0 <= ofs - /\ ofs + Zmax 0 sz <= tsz. + /\ ofs + Z.max 0 sz <= tsz. Definition cenv_separated (cenv: compilenv) (vars: list (ident * Z)) : Prop := forall id1 sz1 ofs1 id2 sz2 ofs2, @@ -901,7 +901,7 @@ Remark assign_variable_incr: Proof. simpl; intros. inv H. generalize (align_le stksz (block_alignment sz) (block_alignment_pos sz)). - assert (0 <= Zmax 0 sz). apply Zmax_bound_l. omega. + assert (0 <= Z.max 0 sz). apply Zmax_bound_l. omega. omega. Qed. @@ -914,7 +914,7 @@ Proof. Opaque assign_variable. destruct a as [id s]. simpl. intros. destruct (assign_variable (cenv, sz) (id, s)) as [cenv1 sz1] eqn:?. - apply Zle_trans with sz1. eapply assign_variable_incr; eauto. eauto. + apply Z.le_trans with sz1. eapply assign_variable_incr; eauto. eauto. Transparent assign_variable. Qed. @@ -925,8 +925,8 @@ Proof. intros; red; intros. apply Zdivides_trans with (block_alignment sz). unfold align_chunk. unfold block_alignment. - generalize Zone_divide; intro. - generalize Zdivide_refl; intro. + generalize Z.divide_1_l; intro. + generalize Z.divide_refl; intro. assert (2 | 4). exists 2; auto. assert (2 | 8). exists 4; auto. assert (4 | 8). exists 2; auto. @@ -942,10 +942,10 @@ Qed. Remark inj_offset_aligned_block': forall stacksize sz, - Mem.inj_offset_aligned (align stacksize (block_alignment sz)) (Zmax 0 sz). + Mem.inj_offset_aligned (align stacksize (block_alignment sz)) (Z.max 0 sz). Proof. intros. - replace (block_alignment sz) with (block_alignment (Zmax 0 sz)). + replace (block_alignment sz) with (block_alignment (Z.max 0 sz)). apply inj_offset_aligned_block. rewrite Zmax_spec. destruct (zlt sz 0); auto. transitivity 1. reflexivity. unfold block_alignment. rewrite zlt_true. auto. omega. diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index 8d6cdb24..036b768b 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -373,15 +373,15 @@ Lemma sizeof_alignof_compat: forall env t, naturally_aligned t -> (alignof env t | sizeof env t). Proof. induction t; intros [A B]; unfold alignof, align_attr; rewrite A; simpl. -- apply Zdivide_refl. -- destruct i; apply Zdivide_refl. +- apply Z.divide_refl. +- destruct i; apply Z.divide_refl. - exists (8 / Archi.align_int64). unfold Archi.align_int64; destruct Archi.ptr64; reflexivity. -- destruct f. apply Zdivide_refl. exists (8 / Archi.align_float64). unfold Archi.align_float64; destruct Archi.ptr64; reflexivity. -- apply Zdivide_refl. +- destruct f. apply Z.divide_refl. exists (8 / Archi.align_float64). unfold Archi.align_float64; destruct Archi.ptr64; reflexivity. +- apply Z.divide_refl. - apply Z.divide_mul_l; auto. -- apply Zdivide_refl. -- destruct (env!i). apply co_sizeof_alignof. apply Zdivide_0. -- destruct (env!i). apply co_sizeof_alignof. apply Zdivide_0. +- apply Z.divide_refl. +- destruct (env!i). apply co_sizeof_alignof. apply Z.divide_0_r. +- destruct (env!i). apply co_sizeof_alignof. apply Z.divide_0_r. Qed. (** ** Size and alignment for composite definitions *) @@ -435,9 +435,9 @@ Lemma sizeof_struct_incr: Proof. induction m as [|[id t]]; simpl; intros. - omega. -- apply Zle_trans with (align cur (alignof env t)). +- apply Z.le_trans with (align cur (alignof env t)). apply align_le. apply alignof_pos. - apply Zle_trans with (align cur (alignof env t) + sizeof env t). + apply Z.le_trans with (align cur (alignof env t) + sizeof env t). generalize (sizeof_pos env t); omega. apply IHm. Qed. @@ -488,7 +488,7 @@ Proof. inv H. inv H0. split. apply align_le. apply alignof_pos. apply sizeof_struct_incr. exploit IHfld; eauto. intros [A B]. split; auto. - eapply Zle_trans; eauto. apply Zle_trans with (align pos (alignof env t)). + eapply Z.le_trans; eauto. apply Z.le_trans with (align pos (alignof env t)). apply align_le. apply alignof_pos. generalize (sizeof_pos env t). omega. Qed. @@ -627,7 +627,7 @@ Fixpoint alignof_blockcopy (env: composite_env) (t: type) : Z := Lemma alignof_blockcopy_1248: forall env ty, let a := alignof_blockcopy env ty in a = 1 \/ a = 2 \/ a = 4 \/ a = 8. Proof. - assert (X: forall co, let a := Zmin 8 (co_alignof co) in + assert (X: forall co, let a := Z.min 8 (co_alignof co) in a = 1 \/ a = 2 \/ a = 4 \/ a = 8). { intros. destruct (co_alignof_two_p co) as [n EQ]. unfold a; rewrite EQ. @@ -635,7 +635,7 @@ Proof. destruct n; auto. destruct n; auto. right; right; right. apply Z.min_l. - rewrite two_power_nat_two_p. rewrite ! inj_S. + rewrite two_power_nat_two_p. rewrite ! Nat2Z.inj_succ. change 8 with (two_p 3). apply two_p_monotone. omega. } induction ty; simpl. @@ -661,28 +661,28 @@ Lemma sizeof_alignof_blockcopy_compat: Proof. assert (X: forall co, (Z.min 8 (co_alignof co) | co_sizeof co)). { - intros. apply Zdivide_trans with (co_alignof co). 2: apply co_sizeof_alignof. + intros. apply Z.divide_trans with (co_alignof co). 2: apply co_sizeof_alignof. destruct (co_alignof_two_p co) as [n EQ]. rewrite EQ. - destruct n. apply Zdivide_refl. - destruct n. apply Zdivide_refl. - destruct n. apply Zdivide_refl. + destruct n. apply Z.divide_refl. + destruct n. apply Z.divide_refl. + destruct n. apply Z.divide_refl. apply Z.min_case. exists (two_p (Z.of_nat n)). change 8 with (two_p 3). rewrite <- two_p_is_exp by omega. - rewrite two_power_nat_two_p. rewrite !inj_S. f_equal. omega. - apply Zdivide_refl. + rewrite two_power_nat_two_p. rewrite !Nat2Z.inj_succ. f_equal. omega. + apply Z.divide_refl. } induction ty; simpl. - apply Zdivide_refl. - apply Zdivide_refl. - apply Zdivide_refl. - apply Zdivide_refl. - apply Zdivide_refl. + apply Z.divide_refl. + apply Z.divide_refl. + apply Z.divide_refl. + apply Z.divide_refl. + apply Z.divide_refl. apply Z.divide_mul_l. auto. - apply Zdivide_refl. - destruct (env!i). apply X. apply Zdivide_0. - destruct (env!i). apply X. apply Zdivide_0. + apply Z.divide_refl. + destruct (env!i). apply X. apply Z.divide_0_r. + destruct (env!i). apply X. apply Z.divide_0_r. Qed. (** Type ranks *) @@ -707,7 +707,7 @@ Fixpoint rank_type (ce: composite_env) (t: type) : nat := Fixpoint rank_members (ce: composite_env) (m: members) : nat := match m with | nil => 0%nat - | (id, t) :: m => Peano.max (rank_type ce t) (rank_members ce m) + | (id, t) :: m => Init.Nat.max (rank_type ce t) (rank_members ce m) end. (** ** C types and back-end types *) @@ -818,7 +818,7 @@ Program Definition composite_of_def co_sizeof_alignof := _ |} end. Next Obligation. - apply Zle_ge. eapply Zle_trans. eapply sizeof_composite_pos. + apply Z.le_ge. eapply Z.le_trans. eapply sizeof_composite_pos. apply align_le; apply alignof_composite_pos. Defined. Next Obligation. diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v index 388b6544..77d6cfea 100644 --- a/cfrontend/Initializers.v +++ b/cfrontend/Initializers.v @@ -186,7 +186,7 @@ Fixpoint transl_init_rec (ce: composite_env) (ty: type) (i: initializer) | Init_single a, _ => do d <- transl_init_single ce ty a; OK (d :: k) | Init_array il, Tarray tyelt nelt _ => - transl_init_array ce tyelt il (Zmax 0 nelt) k + transl_init_array ce tyelt il (Z.max 0 nelt) k | Init_struct il, Tstruct id _ => do co <- lookup_composite ce id; match co_su co with diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index 524bc631..272b929f 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -486,7 +486,7 @@ Inductive tr_init: type -> initializer -> list init_data -> Prop := transl_init_single ge ty a = OK d -> tr_init ty (Init_single a) (d :: nil) | tr_init_arr: forall tyelt nelt attr il d, - tr_init_array tyelt il (Zmax 0 nelt) d -> + tr_init_array tyelt il (Z.max 0 nelt) d -> tr_init (Tarray tyelt nelt attr) (Init_array il) d | tr_init_str: forall id attr il co d, lookup_composite ge id = OK co -> co_su co = Struct -> @@ -723,7 +723,7 @@ Local Opaque sizeof. + rewrite idlsize_app, padding_size. exploit tr_init_size; eauto. intros EQ; rewrite EQ. omega. simpl. unfold lookup_composite in H. destruct (ge.(genv_cenv)!id) as [co'|] eqn:?; inv H. - apply Zle_trans with (sizeof_union ge (co_members co)). + apply Z.le_trans with (sizeof_union ge (co_members co)). eapply union_field_size; eauto. erewrite co_consistent_sizeof by (eapply ce_consistent; eauto). unfold sizeof_composite. rewrite H0. apply align_le. @@ -816,9 +816,9 @@ Lemma store_init_data_list_app: Genv.store_init_data_list ge m b ofs (data1 ++ data2) = Some m''. Proof. induction data1; simpl; intros. - inv H. rewrite Zplus_0_r in H0. auto. + inv H. rewrite Z.add_0_r in H0. auto. destruct (Genv.store_init_data ge m b ofs a); try discriminate. - rewrite Zplus_assoc in H0. eauto. + rewrite Z.add_assoc in H0. eauto. Qed. Remark store_init_data_list_padding: @@ -874,7 +874,7 @@ Local Opaque sizeof. eapply store_init_data_list_app. eauto. rewrite (tr_init_size _ _ _ H9). - rewrite <- Zplus_assoc. eapply H2. eauto. eauto. + rewrite <- Z.add_assoc. eapply H2. eauto. eauto. apply align_le. apply alignof_pos. Qed. diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index 0a191f29..45b686f3 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -80,7 +80,7 @@ Definition initial_generator (x: unit) : generator := Definition gensym (ty: type): mon ident := fun (g: generator) => Res (gen_next g) - (mkgenerator (Psucc (gen_next g)) ((gen_next g, ty) :: gen_trail g)) + (mkgenerator (Pos.succ (gen_next g)) ((gen_next g, ty) :: gen_trail g)) (Ple_succ (gen_next g)). (** Construct a sequence from a list of statements. To facilitate the diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index 8ed924e5..7af499f4 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -604,7 +604,7 @@ Proof. destruct (peq id id0). inv A. right. exploit Mem.alloc_result; eauto. exploit Mem.nextblock_alloc; eauto. generalize (alloc_variables_nextblock _ _ _ _ _ _ H0). intros A B C. - subst b. split. apply Ple_refl. eapply Plt_le_trans; eauto. rewrite B. apply Plt_succ. + subst b. split. apply Ple_refl. eapply Pos.lt_le_trans; eauto. rewrite B. apply Plt_succ. auto. right. exploit Mem.nextblock_alloc; eauto. intros B. rewrite B in A. xomega. Qed. @@ -696,7 +696,7 @@ Proof. (* variable is not lifted out of memory *) exploit Mem.alloc_parallel_inject. - eauto. eauto. apply Zle_refl. apply Zle_refl. + eauto. eauto. apply Z.le_refl. apply Z.le_refl. intros [j1 [tm1 [tb1 [A [B [C [D E]]]]]]]. exploit IHalloc_variables; eauto. instantiate (1 := PTree.set id (tb1, ty) te). intros [j' [te' [tm' [J [K [L [M [N [Q [O P]]]]]]]]]]. @@ -778,8 +778,8 @@ Proof. apply IHalloc_variables. red; intros. rewrite PTree.gsspec in H2. destruct (peq id0 id). inv H2. eapply Mem.load_alloc_same'; eauto. - omega. rewrite Zplus_0_l. eapply sizeof_by_value; eauto. - apply Zdivide_0. + omega. rewrite Z.add_0_l. eapply sizeof_by_value; eauto. + apply Z.divide_0_r. eapply Mem.load_alloc_other; eauto. Qed. @@ -1053,7 +1053,7 @@ Proof. assert (RPSRC: Mem.range_perm m bsrc (Ptrofs.unsigned osrc) (Ptrofs.unsigned osrc + sizeof tge ty) Cur Nonempty). eapply Mem.range_perm_implies. eapply Mem.loadbytes_range_perm; eauto. auto with mem. assert (RPDST: Mem.range_perm m bdst (Ptrofs.unsigned odst) (Ptrofs.unsigned odst + sizeof tge ty) Cur Nonempty). - replace (sizeof tge ty) with (Z_of_nat (length bytes)). + replace (sizeof tge ty) with (Z.of_nat (length bytes)). eapply Mem.range_perm_implies. eapply Mem.storebytes_range_perm; eauto. auto with mem. rewrite LEN. apply nat_of_Z_eq. omega. assert (PSRC: Mem.perm m bsrc (Ptrofs.unsigned osrc) Cur Nonempty). |