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/RTLtoBTLproof.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/RTLtoBTLproof.v')
| -rw-r--r-- | scheduling/RTLtoBTLproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index 60edea49..feaac26f 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -727,9 +727,9 @@ Qed. Local Hint Resolve plus_one star_refl: core. Theorem transf_program_correct: - forward_simulation (RTL.semantics prog) (BTL.semantics tprog). + forward_simulation (RTL.semantics prog) (BTL.cfgsem tprog). Proof. - eapply (Forward_simulation (L1:=RTL.semantics prog) (L2:=semantics tprog) (ltof _ omeasure) match_states). + eapply (Forward_simulation (L1:=RTL.semantics prog) (L2:=cfgsem tprog) (ltof _ omeasure) match_states). constructor 1; simpl. - apply well_founded_ltof. - eapply transf_initial_states. |