diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-20 11:58:40 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-20 11:58:40 +0200 |
| commit | 2408dd1aecf8d8c3bfd3b24a65f7f57cf602cb10 (patch) | |
| tree | b997c709ea92723f55b23b9b2eb23235b6e70dd6 /scheduling/RTLtoBTLproof.v | |
| parent | f37547880890ec7ff2acfba89848944d492ce9ad (diff) | |
| download | compcert-kvx-2408dd1aecf8d8c3bfd3b24a65f7f57cf602cb10.tar.gz compcert-kvx-2408dd1aecf8d8c3bfd3b24a65f7f57cf602cb10.zip | |
Changing to an opaq record in BTL info, this is a broken commit
Diffstat (limited to 'scheduling/RTLtoBTLproof.v')
| -rw-r--r-- | scheduling/RTLtoBTLproof.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index 6681d691..7ad1472b 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -215,7 +215,7 @@ type defined below. Intuitively, each RTL step corresponds to either Fixpoint measure ib: nat := match ib with | Bseq ib1 ib2 - | Bcond _ _ ib1 ib2 _ _ => measure ib1 + measure ib2 + | Bcond _ _ ib1 ib2 _ => measure ib1 + measure ib2 | ib => 1 end. @@ -238,7 +238,7 @@ Lemma entry_isnt_goto dupmap f pc ib: Proof. intros. destruct (entry ib); trivial. - destruct fi; trivial. inv H. inv H4. + destruct fi; trivial. inv H. inv H5. Qed. Lemma expand_entry_isnt_goto dupmap f pc ib: @@ -248,7 +248,7 @@ Proof. destruct (is_goto (expand (entry ib) None))eqn:EQG; destruct (expand (entry ib) None); try destruct fi; try discriminate; trivial. - intros; inv H; inv H4. + intros; inv H; inv H5. Qed. Lemma list_nth_z_rev_dupmap: @@ -499,10 +499,10 @@ Proof. destruct (is_goto ib2) eqn:GT. destruct ib2; try destruct fi; try discriminate. - (* Bgoto *) - inv MSS2. inversion MIB; subst; try inv H3. - remember H0 as ODUPLIC; clear HeqODUPLIC. + inv MSS2. inversion MIB; subst; try inv H4. + remember H2 as ODUPLIC; clear HeqODUPLIC. eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC. - apply DMC in H0 as [ib [FNC MI]]; clear DMC. + apply DMC in H2 as [ib [FNC MI]]; clear DMC. eexists; left; eexists; split. + repeat econstructor; eauto. apply iblock_istep_run_equiv in BTL_RUN; eauto. |