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. --- arm/Asmgenproof.v | 2 +- arm/Conventions1.v | 62 +++++++++++++++++++++++++++--------------------------- arm/Op.v | 4 ++-- arm/Stacklayout.v | 2 +- 4 files changed, 35 insertions(+), 35 deletions(-) (limited to 'arm') diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index c1c3900c..9e6b2c98 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -870,7 +870,7 @@ Opaque loadind. save_lr ra_ofs (Pcfi_rel_offset ra_ofs' :: x0)) in *. set (tf := {| fn_sig := Mach.fn_sig f; fn_code := tfbody |}) in *. 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/arm/Conventions1.v b/arm/Conventions1.v index 86be8c95..c5277e8d 100644 --- a/arm/Conventions1.v +++ b/arm/Conventions1.v @@ -298,7 +298,7 @@ Fixpoint size_arguments_hf (tyl: list typ) (ir fr ofs: Z) {struct tyl} : Z := Fixpoint size_arguments_sf (tyl: list typ) (ofs: Z) {struct tyl} : Z := match tyl with - | nil => Zmax 0 ofs + | nil => Z.max 0 ofs | (Tint | Tsingle | Tany32) :: tys => size_arguments_sf tys (ofs + 1) | (Tfloat | Tlong | Tany64) :: tys => size_arguments_sf tys (align ofs 2 + 2) end. @@ -369,8 +369,8 @@ Proof. destruct (zlt fr 8); destruct H. subst. apply freg_param_caller_save. eapply IHtyl; eauto. - subst. split. apply Zle_ge. apply align_le. omega. auto. - eapply Y; eauto. apply Zle_trans with (align ofs 2). apply align_le; omega. omega. + subst. split. apply Z.le_ge. apply align_le. omega. auto. + eapply Y; eauto. apply Z.le_trans with (align ofs 2). apply align_le; omega. omega. - (* long *) set (ir' := align ir 2) in *. assert (ofs <= align ofs 2) by (apply align_le; omega). @@ -395,17 +395,17 @@ Proof. destruct (zlt fr 8); destruct H. subst. apply freg_param_caller_save. eapply IHtyl; eauto. - subst. split. apply Zle_ge. apply align_le. omega. auto. - eapply Y; eauto. apply Zle_trans with (align ofs 2). apply align_le; omega. omega. + subst. split. apply Z.le_ge. apply align_le. omega. auto. + eapply Y; eauto. apply Z.le_trans with (align ofs 2). apply align_le; omega. omega. Qed. Remark loc_arguments_sf_charact: forall tyl ofs p, - In p (loc_arguments_sf tyl ofs) -> forall_rpair (loc_argument_charact (Zmax 0 ofs)) p. + In p (loc_arguments_sf tyl ofs) -> forall_rpair (loc_argument_charact (Z.max 0 ofs)) p. Proof. - assert (X: forall ofs1 ofs2 l, loc_argument_charact (Zmax 0 ofs2) l -> ofs1 <= ofs2 -> loc_argument_charact (Zmax 0 ofs1) l). + assert (X: forall ofs1 ofs2 l, loc_argument_charact (Z.max 0 ofs2) l -> ofs1 <= ofs2 -> loc_argument_charact (Z.max 0 ofs1) l). { destruct l; simpl; intros; auto. destruct sl; auto. intuition xomega. } - assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_charact (Zmax 0 ofs2)) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_charact (Zmax 0 ofs1)) p). + assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_charact (Z.max 0 ofs2)) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_charact (Z.max 0 ofs1)) p). { destruct p; simpl; intuition eauto. } induction tyl; simpl loc_arguments_sf; intros. elim H. @@ -482,29 +482,29 @@ Proof. induction tyl; simpl; intros. omega. destruct a. - destruct (zlt ir 4); eauto. apply Zle_trans with (ofs0 + 1); auto; omega. + destruct (zlt ir 4); eauto. apply Z.le_trans with (ofs0 + 1); auto; omega. destruct (zlt fr 8); eauto. - apply Zle_trans with (align ofs0 2). apply align_le; omega. - apply Zle_trans with (align ofs0 2 + 2); auto; omega. + apply Z.le_trans with (align ofs0 2). apply align_le; omega. + apply Z.le_trans with (align ofs0 2 + 2); auto; omega. set (ir' := align ir 2). destruct (zlt ir' 4); eauto. - apply Zle_trans with (align ofs0 2). apply align_le; omega. - apply Zle_trans with (align ofs0 2 + 2); auto; omega. + apply Z.le_trans with (align ofs0 2). apply align_le; omega. + apply Z.le_trans with (align ofs0 2 + 2); auto; omega. destruct (zlt fr 8); eauto. - apply Zle_trans with (ofs0 + 1); eauto. omega. - destruct (zlt ir 4); eauto. apply Zle_trans with (ofs0 + 1); auto; omega. + apply Z.le_trans with (ofs0 + 1); eauto. omega. + destruct (zlt ir 4); eauto. apply Z.le_trans with (ofs0 + 1); auto; omega. destruct (zlt fr 8); eauto. - apply Zle_trans with (align ofs0 2). apply align_le; omega. - apply Zle_trans with (align ofs0 2 + 2); auto; omega. + apply Z.le_trans with (align ofs0 2). apply align_le; omega. + apply Z.le_trans with (align ofs0 2 + 2); auto; omega. Qed. Remark size_arguments_sf_above: forall tyl ofs0, - Zmax 0 ofs0 <= size_arguments_sf tyl ofs0. + Z.max 0 ofs0 <= size_arguments_sf tyl ofs0. Proof. induction tyl; simpl; intros. omega. - destruct a; (eapply Zle_trans; [idtac|eauto]). + destruct a; (eapply Z.le_trans; [idtac|eauto]). xomega. assert (ofs0 <= align ofs0 2) by (apply align_le; omega). xomega. assert (ofs0 <= align ofs0 2) by (apply align_le; omega). xomega. @@ -516,9 +516,9 @@ 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. assert (0 <= size_arguments_sf (sig_args s) (-4)). - { change 0 with (Zmax 0 (-4)). apply size_arguments_sf_above. } + { change 0 with (Z.max 0 (-4)). apply size_arguments_sf_above. } assert (0 <= size_arguments_hf (sig_args s) 0 0 0). { apply size_arguments_hf_above. } destruct Archi.abi; [ | destruct (cc_vararg (sig_cc s)) ]; auto. @@ -549,14 +549,14 @@ Proof. destruct H. discriminate. destruct H. discriminate. eauto. destruct Archi.big_endian. destruct H. inv H. - eapply Zle_trans. 2: apply size_arguments_hf_above. simpl; omega. + eapply Z.le_trans. 2: apply size_arguments_hf_above. simpl; omega. destruct H. inv H. - rewrite <- Zplus_assoc. simpl. apply size_arguments_hf_above. + rewrite <- Z.add_assoc. simpl. apply size_arguments_hf_above. eauto. destruct H. inv H. - rewrite <- Zplus_assoc. simpl. apply size_arguments_hf_above. + rewrite <- Z.add_assoc. simpl. apply size_arguments_hf_above. destruct H. inv H. - eapply Zle_trans. 2: apply size_arguments_hf_above. simpl; omega. + eapply Z.le_trans. 2: apply size_arguments_hf_above. simpl; omega. eauto. - (* float *) destruct (zlt fr 8); destruct H. @@ -581,7 +581,7 @@ Qed. Lemma loc_arguments_sf_bounded: forall ofs ty tyl ofs0, In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_sf tyl ofs0)) -> - Zmax 0 (ofs + typesize ty) <= size_arguments_sf tyl ofs0. + Z.max 0 (ofs + typesize ty) <= size_arguments_sf tyl ofs0. Proof. induction tyl; simpl; intros. elim H. @@ -598,15 +598,15 @@ Proof. destruct H. destruct Archi.big_endian. destruct (zlt (align ofs0 2) 0); inv H. - eapply Zle_trans. 2: apply size_arguments_sf_above. simpl; xomega. + eapply Z.le_trans. 2: apply size_arguments_sf_above. simpl; xomega. destruct (zlt (align ofs0 2) 0); inv H. - rewrite <- Zplus_assoc. simpl. apply size_arguments_sf_above. + rewrite <- Z.add_assoc. simpl. apply size_arguments_sf_above. destruct H. destruct Archi.big_endian. destruct (zlt (align ofs0 2) 0); inv H. - rewrite <- Zplus_assoc. simpl. apply size_arguments_sf_above. + rewrite <- Z.add_assoc. simpl. apply size_arguments_sf_above. destruct (zlt (align ofs0 2) 0); inv H. - eapply Zle_trans. 2: apply size_arguments_sf_above. simpl; xomega. + eapply Z.le_trans. 2: apply size_arguments_sf_above. simpl; xomega. eauto. - (* float *) destruct H. @@ -630,7 +630,7 @@ Proof. unfold loc_arguments, size_arguments; intros. assert (In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_sf (sig_args s) (-4))) -> ofs + typesize ty <= size_arguments_sf (sig_args s) (-4)). - { intros. eapply Zle_trans. 2: eapply loc_arguments_sf_bounded; eauto. xomega. } + { intros. eapply Z.le_trans. 2: eapply loc_arguments_sf_bounded; eauto. xomega. } assert (In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_hf (sig_args s) 0 0 0)) -> ofs + typesize ty <= size_arguments_hf (sig_args s) 0 0 0). { intros. eapply loc_arguments_hf_bounded; eauto. } diff --git a/arm/Op.v b/arm/Op.v index 9515557d..60c214d0 100644 --- a/arm/Op.v +++ b/arm/Op.v @@ -522,7 +522,7 @@ End SOUNDNESS. Program Definition mk_shift_amount (n: int) : shift_amount := {| s_amount := Int.modu n Int.iwordsize; s_range := _ |}. Next Obligation. - assert (0 <= Zmod (Int.unsigned n) 32 < 32). apply Z_mod_lt. omega. + assert (0 <= Z.modulo (Int.unsigned n) 32 < 32). apply Z_mod_lt. omega. unfold Int.ltu, Int.modu. change (Int.unsigned Int.iwordsize) with 32. rewrite Int.unsigned_repr. apply zlt_true. omega. assert (32 < Int.max_unsigned). compute; auto. omega. @@ -983,7 +983,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/arm/Stacklayout.v b/arm/Stacklayout.v index 043393bf..462d83ad 100644 --- a/arm/Stacklayout.v +++ b/arm/Stacklayout.v @@ -133,7 +133,7 @@ Proof. set (ol := align (ora + 4) 8); set (ocs := ol + 4 * b.(bound_local)); set (ostkdata := align (size_callee_save_area b ocs) 8). - split. apply Zdivide_0. + split. apply Z.divide_0_r. split. apply align_divides; omega. split. apply align_divides; omega. unfold ora, olink; auto using Z.divide_mul_l, Z.divide_add_r, Z.divide_refl. -- cgit