diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-04-07 14:13:54 +0200 |
---|---|---|
committer | Bernhard Schommer <bschommer@users.noreply.github.com> | 2017-04-28 15:00:03 +0200 |
commit | 53c1757eeb2a76bae796854b9437808ce7ac907e (patch) | |
tree | 9cb8cdb2a3c70496e883bccaed681595529de735 /test/spass/tableau.c | |
parent | 2b3e1f021b2131917cc7a2cf6d3d0d2db9d41ecc (diff) | |
download | compcert-53c1757eeb2a76bae796854b9437808ce7ac907e.tar.gz compcert-53c1757eeb2a76bae796854b9437808ce7ac907e.zip |
Modest optimization of leaf functions (continued)
- Avoid reloading LR before a tail call if we're in a leaf function
- Factor out the code that reloads LR if necessary (function Asmgen.transl_epilogue)
- Factor out the corresponding parts of the proof (Asmgenproof1.transl_epilogue_correct, Asmgenproof.step_simulation)
Diffstat (limited to 'test/spass/tableau.c')
0 files changed, 0 insertions, 0 deletions