diff options
Diffstat (limited to 'scheduling/BTL_SEsimuref.v')
| -rw-r--r-- | scheduling/BTL_SEsimuref.v | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v index d47e53b8..51b562c7 100644 --- a/scheduling/BTL_SEsimuref.v +++ b/scheduling/BTL_SEsimuref.v @@ -32,10 +32,11 @@ Record ristate := }. Definition ris_sreg_get (ris: ristate) r: sval := - match PTree.get r ris with + match PTree.get r (ris_sreg ris) with | None => if ris_input_init ris then fSinput r else fSundef | Some sv => sv end. + Coercion ris_sreg_get: ristate >-> Funclass. Definition ris_sreg_set (ris: ristate) (sreg: PTree.t sval): ristate := @@ -479,10 +480,8 @@ Lemma ris_init_correct ctx: ris_refines ctx ris_init sis_init. Proof. unfold ris_init, sis_init; econstructor; simpl in *; eauto. - + split; destruct 1; econstructor; simpl in *; eauto. + split; destruct 1; econstructor; simpl in *; eauto. congruence. - + destruct 1; simpl in *. unfold ris_sreg_get; simpl. - intros; rewrite PTree.gempty; eauto. Qed. Definition rset_smem rm (ris:ristate): ristate := @@ -655,8 +654,6 @@ Proof. + econstructor; eauto. * erewrite ok_transfer_sis, ok_transfer_ris; eauto. * erewrite ok_transfer_ris; eauto. - * erewrite ok_transfer_ris; simpl; unfold ris_sreg_get; simpl; eauto. - intros; rewrite PTree.gempty. simpl; auto. + econstructor; eauto. * erewrite ok_transfer_sis, ok_transfer_ris; eauto. * erewrite ok_transfer_ris; simpl. |