diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-03-23 19:12:19 +0100 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-03-23 19:12:19 +0100 |
commit | dcb523736e82d72b03fa8d055bf74472dba7345c (patch) | |
tree | 71e797c92d45dca509527043d233c51b2ed8fc86 /cfrontend/SimplExprproof.v | |
parent | 3e953ef41f736ed5b7db699b1adf21d46cb5b8db (diff) | |
parent | 6bf310dd678285dc193798e89fc2c441d8430892 (diff) | |
download | compcert-kvx-dcb523736e82d72b03fa8d055bf74472dba7345c.tar.gz compcert-kvx-dcb523736e82d72b03fa8d055bf74472dba7345c.zip |
Merge branch 'master' into merge_master_8.13.1
PARTIAL MERGE (PARTLY BROKEN).
See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE
WARNING:
interface of va_args and assembly sections have changed
Diffstat (limited to 'cfrontend/SimplExprproof.v')
-rw-r--r-- | cfrontend/SimplExprproof.v | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 9a3f32ec..2d059ddd 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -1449,13 +1449,13 @@ Proof. (* for val *) intros [SL1 [TY1 EV1]]. subst sl. econstructor; split. - right; split. apply star_refl. destruct r; simpl; (contradiction || omega). + right; split. apply star_refl. destruct r; simpl; (contradiction || lia). econstructor; eauto. instantiate (1 := tmps). apply tr_top_val_val; auto. (* for effects *) intros SL1. subst sl. econstructor; split. - right; split. apply star_refl. destruct r; simpl; (contradiction || omega). + right; split. apply star_refl. destruct r; simpl; (contradiction || lia). econstructor; eauto. instantiate (1 := tmps). apply tr_top_base. constructor. (* for set *) @@ -1779,7 +1779,7 @@ Proof. subst; simpl Kseqlist. econstructor; split. right; split. rewrite app_ass. rewrite Kseqlist_app. eexact EXEC. - simpl. omega. + simpl. lia. constructor. (* for value *) exploit tr_simple_lvalue; eauto. intros [SL1 [TY1 EV1]]. @@ -1788,7 +1788,7 @@ Proof. subst; simpl Kseqlist. econstructor; split. right; split. rewrite app_ass. rewrite Kseqlist_app. eexact EXEC. - simpl. omega. + simpl. lia. constructor. (* postincr *) exploit tr_top_leftcontext; eauto. clear H14. @@ -1846,7 +1846,7 @@ Proof. subst. simpl Kseqlist. econstructor; split. right; split. rewrite app_ass; rewrite Kseqlist_app. eexact EXEC. - simpl; omega. + simpl; lia. constructor. (* for value *) exploit tr_simple_lvalue; eauto. intros [SL1 [TY1 EV1]]. @@ -1863,7 +1863,7 @@ Proof. subst sl0; simpl Kseqlist. econstructor; split. right; split. apply star_refl. simpl. apply plus_lt_compat_r. - apply (leftcontext_size _ _ _ H). simpl. omega. + apply (leftcontext_size _ _ _ H). simpl. lia. econstructor; eauto. apply S. eapply tr_expr_monotone; eauto. auto. auto. @@ -1885,7 +1885,7 @@ Proof. (* for effects *) econstructor; split. right; split. apply star_refl. simpl. apply plus_lt_compat_r. - apply (leftcontext_size _ _ _ H). simpl. omega. + apply (leftcontext_size _ _ _ H). simpl. lia. econstructor; eauto. exploit tr_simple_rvalue; eauto. simpl. intros A. subst sl1. apply S. constructor; auto. auto. auto. @@ -2015,12 +2015,12 @@ Proof. inv H6. inv H0. econstructor; split. right; split. apply push_seq. - simpl. omega. + simpl. lia. econstructor; eauto. constructor. auto. (* do 2 *) inv H7. inv H6. inv H. econstructor; split. - right; split. apply star_refl. simpl. omega. + right; split. apply star_refl. simpl. lia. econstructor; eauto. constructor. (* seq *) |