diff options
| author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2017-09-22 19:50:52 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-09-22 19:53:06 +0200 |
| commit | 8d5c6bb8f0cac1339dec7b730997ee30b1517073 (patch) | |
| tree | 3ffd8bcb28a88ae4ff51989aed37b0ad2cb676b2 /backend/Stackingproof.v | |
| parent | 0f210f622a4609811959f4450f770c61f5eb6532 (diff) | |
| download | compcert-kvx-8d5c6bb8f0cac1339dec7b730997ee30b1517073.tar.gz compcert-kvx-8d5c6bb8f0cac1339dec7b730997ee30b1517073.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 'backend/Stackingproof.v')
| -rw-r--r-- | backend/Stackingproof.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index d3d901b6..f7570f57 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -133,7 +133,7 @@ Qed. Remark bound_stack_data_stacksize: f.(Linear.fn_stacksize) <= b.(bound_stack_data). Proof. - unfold b, function_bounds, bound_stack_data. apply Zmax1. + unfold b, function_bounds, bound_stack_data. apply Z.le_max_l. Qed. (** * Memory assertions used to describe the contents of stack frames *) @@ -217,7 +217,7 @@ Proof. - red; intros. apply Mem.perm_implies with Freeable; auto with mem. apply H0. rewrite size_type_chunk, typesize_typesize in H4. omega. - rewrite align_type_chunk. apply Z.divide_add_r. - apply Zdivide_trans with 8; auto. + apply Z.divide_trans with 8; auto. exists (8 / (4 * typealign ty)); destruct ty; reflexivity. apply Z.mul_divide_mono_l. auto. Qed. @@ -962,7 +962,7 @@ Local Opaque mreg_type. assert (SZREC: pos1 + sz <= size_callee_save_area_rec l (pos1 + sz)) by (apply size_callee_save_area_rec_incr). assert (POS1: pos <= pos1) by (apply align_le; auto). assert (AL1: (align_chunk (chunk_of_type ty) | pos1)). - { unfold pos1. apply Zdivide_trans with sz. + { unfold pos1. apply Z.divide_trans with sz. unfold sz; rewrite <- size_type_chunk. apply align_size_chunk_divides. apply align_divides; auto. } apply range_drop_left with (mid := pos1) in SEP; [ | omega ]. @@ -1984,7 +1984,7 @@ Proof. econstructor; eauto with coqlib. apply Val.Vptr_has_type. intros; red. - apply Zle_trans with (size_arguments (Linear.funsig f')); auto. + apply Z.le_trans with (size_arguments (Linear.funsig f')); auto. apply loc_arguments_bounded; auto. simpl; red; auto. simpl. rewrite sep_assoc. exact SEP. |