aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling/BTLtoRTLproof.v
diff options
context:
space:
mode:
Diffstat (limited to 'scheduling/BTLtoRTLproof.v')
-rw-r--r--scheduling/BTLtoRTLproof.v12
1 files changed, 10 insertions, 2 deletions
diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v
index bbb984c4..14e986aa 100644
--- a/scheduling/BTLtoRTLproof.v
+++ b/scheduling/BTLtoRTLproof.v
@@ -390,8 +390,8 @@ Proof.
+ inv H1. econstructor; eauto.
Qed.
-Theorem transf_program_correct:
- forward_simulation (semantics prog) (RTL.semantics tprog).
+Theorem transf_program_correct_cfg:
+ forward_simulation (BTL.cfgsem prog) (RTL.semantics tprog).
Proof.
eapply forward_simulation_plus with match_states.
- eapply senv_preserved.
@@ -400,4 +400,12 @@ Proof.
- eapply plus_simulation.
Qed.
+Theorem transf_program_correct:
+ forward_simulation (BTL.fsem prog) (RTL.semantics tprog).
+Proof.
+ eapply compose_forward_simulations.
+ - eapply fsem2cfgsem.
+ - eapply transf_program_correct_cfg.
+Qed.
+
End RTL_SIMULATES_BTL.