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 /cparser | |
| parent | 9b31f673da13a4f4d04d937ac2b9e934c9b8291d (diff) | |
| download | compcert-fb44646eb7308c1dd6a44b85415528982083200b.tar.gz compcert-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 'cparser')
0 files changed, 0 insertions, 0 deletions