diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-28 10:40:54 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-28 10:40:54 +0200 |
| commit | 43ab0b948ac379e55bbe334a0a541c1680437fbf (patch) | |
| tree | 99e40dae20f6ae36c955e96684cc52cdcdf18156 /scheduling/BTLtoRTLproof.v | |
| parent | e30376ce891d0710757c65e85a24e7d2550a37ed (diff) | |
| download | compcert-kvx-43ab0b948ac379e55bbe334a0a541c1680437fbf.tar.gz compcert-kvx-43ab0b948ac379e55bbe334a0a541c1680437fbf.zip | |
most of the proof BTL.fsem -> BTL.cfgsem.
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. |