diff options
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 b08c3ad7..d763c98c 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) := @@ -579,7 +579,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... @@ -636,7 +636,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. |