diff options
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)) |