From 8d5c6bb8f0cac1339dec7b730997ee30b1517073 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 22 Sep 2017 19:50:52 +0200 Subject: Remove coq warnings (#28) Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts. --- x86/Asmgenproof.v | 2 +- x86/Conventions1.v | 20 ++++++++++---------- x86/Op.v | 2 +- x86/Stacklayout.v | 2 +- 4 files changed, 13 insertions(+), 13 deletions(-) (limited to 'x86') diff --git a/x86/Asmgenproof.v b/x86/Asmgenproof.v index 6caf4531..38816fd2 100644 --- a/x86/Asmgenproof.v +++ b/x86/Asmgenproof.v @@ -825,7 +825,7 @@ Transparent destroyed_by_jumptable. destruct (zlt Ptrofs.max_unsigned (list_length_z (fn_code x0))); inv EQ1. monadInv EQ0. rewrite transl_code'_transl_code in EQ1. unfold store_stack in *. - exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. + exploit Mem.alloc_extends. eauto. eauto. apply Z.le_refl. apply Z.le_refl. intros [m1' [C D]]. exploit Mem.storev_extends. eexact D. eexact H1. eauto. eauto. intros [m2' [F G]]. diff --git a/x86/Conventions1.v b/x86/Conventions1.v index ecfb85bf..646c4afb 100644 --- a/x86/Conventions1.v +++ b/x86/Conventions1.v @@ -299,7 +299,7 @@ Proof. assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_64_charact ofs2) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_64_charact ofs1) p). { destruct p; simpl; intuition eauto. } assert (Z: forall ofs, (2 | ofs) -> (2 | ofs + 2)). - { intros. apply Z.divide_add_r; auto. apply Zdivide_refl. } + { intros. apply Z.divide_add_r; auto. apply Z.divide_refl. } Opaque list_nth_z. induction tyl; simpl loc_arguments_64; intros. elim H. @@ -339,10 +339,10 @@ Proof. assert (X: forall l, loc_argument_64_charact 0 l -> loc_argument_acceptable l). { unfold loc_argument_64_charact, loc_argument_acceptable. destruct l as [r | [] ofs ty]; auto. intros [C|C]; auto. - intros [C D]. split; auto. apply Zdivide_trans with 2; auto. + intros [C D]. split; auto. apply Z.divide_trans with 2; auto. exists (2 / typealign ty); destruct ty; reflexivity. } - exploit loc_arguments_64_charact; eauto using Zdivide_0. + exploit loc_arguments_64_charact; eauto using Z.divide_0_r. unfold forall_rpair; destruct p; intuition auto. - (* 32 bits *) assert (X: forall l, loc_argument_32_charact 0 l -> loc_argument_acceptable l). @@ -360,7 +360,7 @@ Remark size_arguments_32_above: Proof. induction tyl; simpl; intros. omega. - apply Zle_trans with (ofs0 + typesize a); auto. + apply Z.le_trans with (ofs0 + typesize a); auto. generalize (typesize_pos a); omega. Qed. @@ -376,21 +376,21 @@ Proof. | None => size_arguments_64 tyl ir fr (ofs0 + 2) end). { destruct (list_nth_z int_param_regs ir); eauto. - apply Zle_trans with (ofs0 + 2); auto. omega. } + apply Z.le_trans with (ofs0 + 2); auto. omega. } assert (B: ofs0 <= match list_nth_z float_param_regs fr with | Some _ => size_arguments_64 tyl ir (fr + 1) ofs0 | None => size_arguments_64 tyl ir fr (ofs0 + 2) end). { destruct (list_nth_z float_param_regs fr); eauto. - apply Zle_trans with (ofs0 + 2); auto. omega. } + apply Z.le_trans with (ofs0 + 2); auto. omega. } destruct a; auto. Qed. Lemma size_arguments_above: forall s, size_arguments s >= 0. Proof. - intros; unfold size_arguments. apply Zle_ge. + intros; unfold size_arguments. apply Z.le_ge. destruct Archi.ptr64; [apply size_arguments_64_above|apply size_arguments_32_above]. Qed. @@ -402,7 +402,7 @@ Proof. induction tyl as [ | t l]; simpl; intros x IN. - contradiction. - rewrite in_app_iff in IN; destruct IN as [IN|IN]. -+ apply Zle_trans with (x + typesize t); [|apply size_arguments_32_above]. ++ apply Z.le_trans with (x + typesize t); [|apply size_arguments_32_above]. Ltac decomp := match goal with | [ H: _ \/ _ |- _ ] => destruct H; decomp @@ -437,7 +437,7 @@ Proof. { intros. destruct (list_nth_z int_param_regs ir); simpl in H0; destruct H0. - discriminate. - eapply IHtyl; eauto. - - inv H0. apply Zle_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above. + - inv H0. apply Z.le_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above. - eapply IHtyl; eauto. } assert (B: forall ty0, In (S Outgoing ofs ty) (regs_of_rpairs @@ -454,7 +454,7 @@ Proof. { intros. destruct (list_nth_z float_param_regs fr); simpl in H0; destruct H0. - discriminate. - eapply IHtyl; eauto. - - inv H0. apply Zle_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above. + - inv H0. apply Z.le_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above. - eapply IHtyl; eauto. } destruct a; eauto. Qed. diff --git a/x86/Op.v b/x86/Op.v index 136c900b..02b04574 100644 --- a/x86/Op.v +++ b/x86/Op.v @@ -1311,7 +1311,7 @@ Remark weak_valid_pointer_no_overflow_extends: Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> 0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned. Proof. - intros. inv H. rewrite Zplus_0_r. apply Ptrofs.unsigned_range_2. + intros. inv H. rewrite Z.add_0_r. apply Ptrofs.unsigned_range_2. Qed. Remark valid_different_pointers_extends: diff --git a/x86/Stacklayout.v b/x86/Stacklayout.v index 22c68099..d375febf 100644 --- a/x86/Stacklayout.v +++ b/x86/Stacklayout.v @@ -140,7 +140,7 @@ Proof. set (oretaddr := align (ostkdata + b.(bound_stack_data)) w). assert (0 < w) by (unfold w; destruct Archi.ptr64; omega). replace (align_chunk Mptr) with w by (rewrite align_chunk_Mptr; auto). - split. apply Zdivide_0. + split. apply Z.divide_0_r. split. apply align_divides; omega. split. apply align_divides; omega. split. apply align_divides; omega. -- cgit