diff options
Diffstat (limited to 'aarch64/Asmblockprops.v')
| -rw-r--r-- | aarch64/Asmblockprops.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/aarch64/Asmblockprops.v b/aarch64/Asmblockprops.v index 782d8aee..d1015ea9 100644 --- a/aarch64/Asmblockprops.v +++ b/aarch64/Asmblockprops.v @@ -25,8 +25,13 @@ Require Import Axioms. Definition bblock_simu (lk: aarch64_linker) (ge: Genv.t fundef unit) (f: function) (bb bb': bblock) := forall rs m rs' m' t, - exec_bblock lk ge f bb rs m t rs' m' -> exec_bblock lk ge f bb rs m t rs' m'. + exec_bblock lk ge f bb rs m t rs' m' -> exec_bblock lk ge f bb' rs m t rs' m'. +Definition bblock_simu_aux (lk: aarch64_linker) (ge: Genv.t fundef unit) (f: function) (bb bb': bblock) := + forall rs m, + bbstep lk ge f bb rs m <> Stuck -> + bbstep lk ge f bb rs m = bbstep lk ge f bb' rs m. + Hint Extern 2 (_ <> _) => congruence: asmgen. Lemma preg_of_data: |