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 /cfrontend | |
| parent | 35ba7f373963d8a1f0094abd457809d1e3c3cdb4 (diff) | |
| download | compcert-kvx-8587b8310a91702e2635a689e1622a87b7bf8985.tar.gz compcert-kvx-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 'cfrontend')
0 files changed, 0 insertions, 0 deletions