diff options
author | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-30 17:14:46 +0200 |
---|---|---|
committer | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-30 17:14:46 +0200 |
commit | 388710f767cc4e4c962c38e962262f35a482bd23 (patch) | |
tree | 6bc313a2efc73d3e90b4483c94d6424e214c1591 /backend | |
parent | 6d9bc90c8912b6b0b8333b874fca8328a6159996 (diff) | |
download | compcert-kvx-388710f767cc4e4c962c38e962262f35a482bd23.tar.gz compcert-kvx-388710f767cc4e4c962c38e962262f35a482bd23.zip |
Minor cleanup of find_instr_bblock
- Remove one auto-generated name
- Move assertion on n's size up
- Clear unnecessary hypothesis (iirc generalize worked better than
exploit here)
- Rewrite progress of Asm.find_instr only in the case that needs it
Diffstat (limited to 'backend')
0 files changed, 0 insertions, 0 deletions