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 /config_x86_64.sh | |
| 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 'config_x86_64.sh')
0 files changed, 0 insertions, 0 deletions