diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-06-14 19:02:39 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-06-14 19:02:39 +0200 |
| commit | 26d9fbb36b2e9c8f1262250035cd804bf87f7228 (patch) | |
| tree | 86ed9c9614b30de04e679745329d575fd912d1d7 /scheduling/BTL_Livecheck.v | |
| parent | 8252a8b7678ca4b82191ce0159b93b976f8c58d9 (diff) | |
| download | compcert-kvx-26d9fbb36b2e9c8f1262250035cd804bf87f7228.tar.gz compcert-kvx-26d9fbb36b2e9c8f1262250035cd804bf87f7228.zip | |
Preparation for scheduling proof, main lemmas ok
Diffstat (limited to 'scheduling/BTL_Livecheck.v')
| -rw-r--r-- | scheduling/BTL_Livecheck.v | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/scheduling/BTL_Livecheck.v b/scheduling/BTL_Livecheck.v index 25a1c545..9f96e74e 100644 --- a/scheduling/BTL_Livecheck.v +++ b/scheduling/BTL_Livecheck.v @@ -583,7 +583,6 @@ Lemma cfgsem2fsem_ibistep_simu_Some sp f stk1 stk2 ib: forall s t rs1 m rs1' m' alive1 oalive2 rs2 (REGS: eqlive_reg (ext alive1) rs1 rs2) (BDY: body_checker (fn_code f) ib alive1 = Some (oalive2)) (LIVE: liveness_ok_function f) - (*(PC : (fn_code f) ! pc = Some ibf)*) (STACKS: list_forall2 eqlive_stackframes stk1 stk2), exists rs2' s', iblock_istep_run ge sp ib rs2 m = Some (out rs2' m' (Some fin)) |