diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-11 17:17:02 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-11 17:17:02 +0200 |
| commit | 6199b498cc309d371ba773966a34ff6a9ee47c2e (patch) | |
| tree | 4a4959a754279e4b291fa9c019aa52e85cbc918d /scheduling | |
| parent | 9c01536d6bb0696091228cb4a4d52cdcd0c55416 (diff) | |
| download | compcert-kvx-6199b498cc309d371ba773966a34ff6a9ee47c2e.tar.gz compcert-kvx-6199b498cc309d371ba773966a34ff6a9ee47c2e.zip | |
stub match_states
Diffstat (limited to 'scheduling')
| -rw-r--r-- | scheduling/BTL_Schedulerproof.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/scheduling/BTL_Schedulerproof.v b/scheduling/BTL_Schedulerproof.v index c8c2a76f..3811b170 100644 --- a/scheduling/BTL_Schedulerproof.v +++ b/scheduling/BTL_Schedulerproof.v @@ -22,10 +22,12 @@ Hypothesis TRANSL: match_prog prog tprog. Let pge := Genv.globalenv prog. Let tpge := Genv.globalenv tprog. +Inductive match_states (s1 s2: BTL.state): Prop :=. (* STUB *) + Theorem transf_program_correct: forward_simulation (fsem prog) (fsem tprog). Proof. - eapply forward_simulation_step with equiv_state. (* lock-step with respect to equiv_states *) + eapply forward_simulation_step with match_states. (* lock-step with respect to match_states *) Admitted. End PRESERVATION. |