diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-01 13:18:32 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-01 14:53:56 +0100 |
| commit | a781244930ababd25e40c40e8df8bd437f3fbf8c (patch) | |
| tree | b5222bc32623c7ec58c66178f22afc3c9a2e065f /scheduling/BTL_SEsimuref.v | |
| parent | 20cdd9c6c3962f7bec5c85719cfa7b0ee22f0100 (diff) | |
| parent | a79f0f99831aa0b0742bf7cce459cc9353bd7cd0 (diff) | |
| download | compcert-kvx-a781244930ababd25e40c40e8df8bd437f3fbf8c.tar.gz compcert-kvx-a781244930ababd25e40c40e8df8bd437f3fbf8c.zip | |
Merge remote-tracking branch 'absint/master' into towards_3.10
Mostly changes in PTree
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. |