diff options
Diffstat (limited to 'scheduling/BTLtoRTLproof.v')
-rw-r--r-- | scheduling/BTLtoRTLproof.v | 12 |
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. |