diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-07-07 10:41:45 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-07-08 07:18:35 +0200 |
| commit | 988070c7bf7109aa1342a99e08b0cc1ddeea9ebb (patch) | |
| tree | 51cbc70d70dad17ae78ba8c9405de146179461eb /common | |
| parent | 26eeda87795cee0a387d58cf4ff8ffa9f63039ba (diff) | |
| download | compcert-kvx-988070c7bf7109aa1342a99e08b0cc1ddeea9ebb.tar.gz compcert-kvx-988070c7bf7109aa1342a99e08b0cc1ddeea9ebb.zip | |
Characterizing Op dependency on memory
Diffstat (limited to 'common')
| -rw-r--r-- | common/Memory.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/common/Memory.v b/common/Memory.v index cd8a2001..65f36966 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -1322,6 +1322,18 @@ Proof. eapply load_store_same. eassumption. Qed. + +Theorem storev_preserv_valid (b : block) (ofs: Z): valid_pointer m1 b ofs = valid_pointer m2 b ofs. +Proof. + unfold storev in STORE. + cut (valid_pointer m1 b ofs = true <-> valid_pointer m2 b ofs = true). + { destruct (valid_pointer _ _ _), (valid_pointer _ _ _); intuition congruence. } + destruct addr; try congruence. + rewrite! valid_pointer_valid_access. split. + - intros; eapply store_valid_access_1; eauto. + - intros; eapply store_valid_access_2; eauto. +Qed. + End STOREV. Lemma load_store_overlap: |