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