From 43ab0b948ac379e55bbe334a0a541c1680437fbf Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Fri, 28 May 2021 10:40:54 +0200 Subject: most of the proof BTL.fsem -> BTL.cfgsem. --- scheduling/BTL_SEtheory.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'scheduling/BTL_SEtheory.v') diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index 79db99c8..c9f50d66 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -633,7 +633,7 @@ Fixpoint transfer_sreg (inputs: list reg) (sreg: reg -> sval): reg -> sval := | r1::l => fun r => if Pos.eq_dec r r1 then sreg r1 else transfer_sreg l sreg r end. -Definition str_inputs (f:function) (tbl: list exit) (or:option reg) := transfer_sreg (Regset.elements (inputs_exit f tbl or)). +Definition str_inputs (f:function) (tbl: list exit) (or:option reg) := transfer_sreg (Regset.elements (pre_inputs f tbl or)). Lemma str_inputs_correct ctx sis rs tbl or r: (forall r : reg, eval_sval ctx (si_sreg sis r) = Some rs # r) -> -- cgit