diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-28 10:40:54 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-28 10:40:54 +0200 |
| commit | 43ab0b948ac379e55bbe334a0a541c1680437fbf (patch) | |
| tree | 99e40dae20f6ae36c955e96684cc52cdcdf18156 /scheduling/BTL_SEtheory.v | |
| parent | e30376ce891d0710757c65e85a24e7d2550a37ed (diff) | |
| download | compcert-kvx-43ab0b948ac379e55bbe334a0a541c1680437fbf.tar.gz compcert-kvx-43ab0b948ac379e55bbe334a0a541c1680437fbf.zip | |
most of the proof BTL.fsem -> BTL.cfgsem.
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) -> |