diff options
Diffstat (limited to 'scheduling/BTL_SEtheory.v')
| -rw-r--r-- | scheduling/BTL_SEtheory.v | 2 |
1 files changed, 1 insertions, 1 deletions
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) -> |