diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-06-22 16:39:53 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-06-22 16:39:53 +0200 |
| commit | fb44646eb7308c1dd6a44b85415528982083200b (patch) | |
| tree | 46d088a96e09516a5b94693099b408361aebf691 /common/Separation.v | |
| parent | 9b31f673da13a4f4d04d937ac2b9e934c9b8291d (diff) | |
| download | compcert-kvx-fb44646eb7308c1dd6a44b85415528982083200b.tar.gz compcert-kvx-fb44646eb7308c1dd6a44b85415528982083200b.zip | |
Stricter control of permissions in memory injections and extensions
As suggested by Lennart Beringer, this commits strengthens memory injections and extensions so as to guarantee that the permissions of existing memory locations are not increased by the injection/extension. The only increase of permissions permitted is empty locations in the source memory state of the injection/extension being mapped to nonempty locations.
Diffstat (limited to 'common/Separation.v')
| -rw-r--r-- | common/Separation.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/common/Separation.v b/common/Separation.v index 4d87443b..6a7ffbea 100644 --- a/common/Separation.v +++ b/common/Separation.v @@ -627,6 +627,10 @@ Next Obligation. - intros. eapply Mem.valid_block_unchanged_on; eauto. - assumption. - assumption. +- intros. destruct (Mem.perm_dec m0 b1 ofs Max Nonempty); auto. + eapply mi_perm_inv; eauto. + eapply Mem.perm_unchanged_on_2; eauto. + eapply IMG; eauto. Qed. Next Obligation. eapply Mem.valid_block_inject_2; eauto. |