diff options
| author | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-09-21 15:31:35 +0200 |
|---|---|---|
| committer | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-09-21 15:40:09 +0200 |
| commit | f2059eb9fd40418a4957d278e42abecf22f171aa (patch) | |
| tree | 4fb9bdf04fbd1a4cb47dc76cbafad018f879b6c4 /aarch64/DuplicateOpcodeHeuristic.ml | |
| parent | 92a8a4c4a8e8106d8e787f0bdfb7d8cddcc019fb (diff) | |
| download | compcert-kvx-f2059eb9fd40418a4957d278e42abecf22f171aa.tar.gz compcert-kvx-f2059eb9fd40418a4957d278e42abecf22f171aa.zip | |
Proof of exec_body_simulation_plus
Added exec_body_simulation_star' in order to prove it.
exec_body_simulation_star' could also be used to prove
exec_body_simulation_star directly (without using
exec_body_simulation_plus). However, at least the way I did it the proof
turns out to be longer.
eexec_body_simulation_plus is still required/useful for
exec_bblock_simulation.
Diffstat (limited to 'aarch64/DuplicateOpcodeHeuristic.ml')
0 files changed, 0 insertions, 0 deletions