diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-11 11:41:37 +0200 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-11 11:41:37 +0200 |
commit | af16cdae6d58033cc8aa06bca330f98b96ba12f2 (patch) | |
tree | 4985e9ae8fa0d580bbf95a198edeca4f0bd6ff46 /cfrontend/Cexec.v | |
parent | 21c979fce33b068ce4b86e67d3d866b203411c6c (diff) | |
parent | 02b169b444c435b8d1aacf54969dd7de57317a5c (diff) | |
download | compcert-kvx-af16cdae6d58033cc8aa06bca330f98b96ba12f2.tar.gz compcert-kvx-af16cdae6d58033cc8aa06bca330f98b96ba12f2.zip |
Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into BTL
Diffstat (limited to 'cfrontend/Cexec.v')
-rw-r--r-- | cfrontend/Cexec.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index fbf9bbeb..24f10b68 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -290,7 +290,7 @@ Definition assign_copy_ok (ty: type) (b: block) (ofs: ptrofs) (b': block) (ofs': Remark check_assign_copy: forall (ty: type) (b: block) (ofs: ptrofs) (b': block) (ofs': ptrofs), { assign_copy_ok ty b ofs b' ofs' } + {~ assign_copy_ok ty b ofs b' ofs' }. -Proof with try (right; intuition omega). +Proof with try (right; intuition lia). intros. unfold assign_copy_ok. destruct (Zdivide_dec (alignof_blockcopy ge ty) (Ptrofs.unsigned ofs')); auto... destruct (Zdivide_dec (alignof_blockcopy ge ty) (Ptrofs.unsigned ofs)); auto... @@ -306,8 +306,8 @@ Proof with try (right; intuition omega). destruct (zeq (Ptrofs.unsigned ofs') (Ptrofs.unsigned ofs)); auto. destruct (zle (Ptrofs.unsigned ofs' + sizeof ge ty) (Ptrofs.unsigned ofs)); auto. destruct (zle (Ptrofs.unsigned ofs + sizeof ge ty) (Ptrofs.unsigned ofs')); auto. - right; intuition omega. - destruct Y... left; intuition omega. + right; intuition lia. + destruct Y... left; intuition lia. Defined. Definition do_assign_loc (w: world) (ty: type) (m: mem) (b: block) (ofs: ptrofs) (v: val): option (world * trace * mem) := @@ -584,7 +584,7 @@ Proof with try congruence. replace (Vlong Int64.zero) with Vnullptr. split; constructor. unfold Vnullptr; rewrite H0; auto. + destruct vargs... mydestr. - split. apply SIZE in Heqo0. econstructor; eauto. congruence. omega. + split. apply SIZE in Heqo0. econstructor; eauto. congruence. lia. constructor. - (* EF_memcpy *) unfold do_ef_memcpy. destruct vargs... destruct v... destruct vargs... @@ -643,7 +643,7 @@ Proof. inv H0. erewrite SIZE by eauto. rewrite H1, H2. auto. - (* EF_free *) inv H; unfold do_ef_free. -+ inv H0. rewrite H1. erewrite SIZE by eauto. rewrite zlt_true. rewrite H3. auto. omega. ++ inv H0. rewrite H1. erewrite SIZE by eauto. rewrite zlt_true. rewrite H3. auto. lia. + inv H0. unfold Vnullptr; destruct Archi.ptr64; auto. - (* EF_memcpy *) inv H; unfold do_ef_memcpy. |