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 /exportclight | |
| parent | 2b3e1f021b2131917cc7a2cf6d3d0d2db9d41ecc (diff) | |
| download | compcert-kvx-53c1757eeb2a76bae796854b9437808ce7ac907e.tar.gz compcert-kvx-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 'exportclight')
0 files changed, 0 insertions, 0 deletions