diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-05-07 08:37:05 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-05-07 08:37:05 +0200 |
| commit | 579ce1d6d18371b753fff2dac7305e13b85b8cab (patch) | |
| tree | 68879b84ccfabf0424178c4ad046ebd97461d8c2 /mppa_k1c/lib | |
| parent | 3be0a8daa9ed0e787d1e4b26092aea4a496b88fd (diff) | |
| download | compcert-kvx-579ce1d6d18371b753fff2dac7305e13b85b8cab.tar.gz compcert-kvx-579ce1d6d18371b753fff2dac7305e13b85b8cab.zip | |
generalize bblock_equiv into bblock_simu
Diffstat (limited to 'mppa_k1c/lib')
| -rw-r--r-- | mppa_k1c/lib/Asmblockgenproof0.v | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v index a8da1cf1..e0780b9d 100644 --- a/mppa_k1c/lib/Asmblockgenproof0.v +++ b/mppa_k1c/lib/Asmblockgenproof0.v @@ -21,11 +21,10 @@ Module AB:=Asmvliw. Hint Extern 2 (_ <> _) => congruence: asmgen. -Inductive bblock_equiv (ge: Genv.t fundef unit) (f: function) (bb bb': bblock) := - | bblock_equiv_intro: - (forall rs m, - exec_bblock ge f bb rs m = exec_bblock ge f bb' rs m) -> - bblock_equiv ge f bb bb'. +Definition bblock_simu (ge: Genv.t fundef unit) (f: function) (bb bb': bblock) := + forall rs m, + exec_bblock ge f bb rs m <> Stuck -> + exec_bblock ge f bb rs m = exec_bblock ge f bb' rs m. Lemma ireg_of_eq: forall r r', ireg_of r = OK r' -> preg_of r = IR r'. |