diff options
| author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2020-03-02 10:32:07 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-02 10:32:07 +0100 |
| commit | 8587b8310a91702e2635a689e1622a87b7bf8985 (patch) | |
| tree | 94bdc25bb7ad1c3b6ff79c0f9587ae3c98a12c0f /backend | |
| parent | 35ba7f373963d8a1f0094abd457809d1e3c3cdb4 (diff) | |
| download | compcert-8587b8310a91702e2635a689e1622a87b7bf8985.tar.gz compcert-8587b8310a91702e2635a689e1622a87b7bf8985.zip | |
Weaker ec_readonly condition over external calls (#225)
Currently we require the memory to be unchanged on readonly locations.
This is too strong. For example, current permissions could decrease
from readonly to none.
This commit weakens the ec_readonly condition to the strict minimum
needed to show the correctness of value analysis for const globals.
Diffstat (limited to 'backend')
| -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 2b233900..b0ce019c 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -1039,9 +1039,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. |