diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-03 16:57:52 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-03 16:57:52 +0100 |
| commit | fe0862b9bb1c9deeb1ea1393889c294fc2cc2ebe (patch) | |
| tree | 50a6ecbb87438cfc21461b4f5066edcf28f8b14e /backend/ValueAnalysis.v | |
| parent | 1ab7b51c30e1b10ac45b0bd64cefdc01da0f7f68 (diff) | |
| parent | 3b640f041be480b82f1b3a1f695ed8a57193bf28 (diff) | |
| download | compcert-kvx-fe0862b9bb1c9deeb1ea1393889c294fc2cc2ebe.tar.gz compcert-kvx-fe0862b9bb1c9deeb1ea1393889c294fc2cc2ebe.zip | |
fixed CSE2 for mppa_k1c
Merge branch 'dm-cse2-naive' of https://github.com/monniaux/CompCert into mppa-cse2
Diffstat (limited to 'backend/ValueAnalysis.v')
| -rw-r--r-- | backend/ValueAnalysis.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index 9a33768c..e25d2e5f 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -1044,9 +1044,8 @@ Proof. red; simpl; intros. destruct (plt b (Mem.nextblock m)). exploit RO; eauto. intros (R & P & Q). split; auto. - split. apply bmatch_incr with bc; auto. apply bmatch_inv with m; auto. - intros. eapply Mem.loadbytes_unchanged_on_1. eapply external_call_readonly; eauto. - auto. intros; red. apply Q. + split. apply bmatch_incr with bc; auto. apply bmatch_ext with m; auto. + intros. eapply external_call_readonly with (m2 := m'); eauto. intros; red; intros; elim (Q ofs). eapply external_call_max_perm with (m2 := m'); eauto. destruct (j' b); congruence. |