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 /backend/ValueDomain.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 'backend/ValueDomain.v')
| -rw-r--r-- | backend/ValueDomain.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 8b76f44d..3c80d733 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -3766,6 +3766,9 @@ Proof. - (* overflow *) intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. rewrite Zplus_0_r. split. omega. apply Int.unsigned_range_2. +- (* perm inv *) + intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. + rewrite Zplus_0_r in H2. auto. Qed. Lemma inj_of_bc_preserves_globals: |