diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-07-24 11:42:09 +0200 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-07-24 11:42:09 +0200 |
commit | a4570fed198034e535d0d6d99e23cfbb1d40b926 (patch) | |
tree | e4e5a9dc845fc0972622ae05fd9084234ed9a44d /backend/ValueAnalysis.v | |
parent | 95f918c38b1e59f40ae7af455ec2c6746289375e (diff) | |
parent | b5c4192c73d7b02e0c90354e26b35a84ee141083 (diff) | |
download | compcert-kvx-a4570fed198034e535d0d6d99e23cfbb1d40b926.tar.gz compcert-kvx-a4570fed198034e535d0d6d99e23cfbb1d40b926.zip |
Merge branch 'kvx-work' into rtl-tunneling
Diffstat (limited to 'backend/ValueAnalysis.v')
-rw-r--r-- | backend/ValueAnalysis.v | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index 561e94c9..e20edff7 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -1287,13 +1287,11 @@ Proof. eapply sound_succ_state; eauto. simpl; auto. unfold transfer; rewrite H. eauto. apply ematch_update; auto. - unfold default_notrap_load_value. constructor. - (* load notrap2 *) eapply sound_succ_state; eauto. simpl; auto. unfold transfer; rewrite H. eauto. apply ematch_update; auto. - unfold default_notrap_load_value. constructor. - (* store *) exploit eval_static_addressing_sound; eauto with va. intros VMADDR. |