aboutsummaryrefslogtreecommitdiffstats
path: root/pg
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2018-06-01 16:52:02 +0200
committerXavier Leroy <xavier.leroy@inria.fr>2018-06-01 16:52:02 +0200
commitc58b421571b0354eea602adbdae674bd1f4847e3 (patch)
tree8c83d3d7428097523d8af00b9abdcf117532be30 /pg
parent24951d885fbadb8f2fa96ea44a6d3b2a397eab00 (diff)
downloadcompcert-c58b421571b0354eea602adbdae674bd1f4847e3.tar.gz
compcert-c58b421571b0354eea602adbdae674bd1f4847e3.zip
Model external calls as destroying all caller-save registers
The semantics of external function calls in LTL, Linear, Mach and Asm now consider that all caller-save registers are set to Vundef by the call. This models that fact that the external function can modify those registers arbitrarily. Update the proofs of the Allocation, Tunneling, Stacking and Asmgen passes accordingly.
Diffstat (limited to 'pg')
0 files changed, 0 insertions, 0 deletions