diff options
Diffstat (limited to 'scheduling/RTLtoBTLproof.v')
| -rw-r--r-- | scheduling/RTLtoBTLproof.v | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index 8a352434..13ba5a29 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -123,12 +123,15 @@ Lemma normRTLrec_iblock_istep_correct tge sp ib rs0 m0 rs1 m1 ofin1: iblock_istep tge sp rs0 m0 (normRTLrec ib k) rs2 m2 ofin2. Proof. induction 1; simpl; intuition subst; eauto. - { (* Bnop *) autodestruct; eauto. } - 1-3: (* Bop, Bload, Bstore *) - intros; repeat econstructor; eauto. - (* Bcond *) - destruct ofin; intuition subst; - destruct b; eapply IHISTEP; eauto. + - (* Bnop *) autodestruct; eauto. + - (* Bop *) repeat econstructor; eauto. + - (* Bload *) inv LOAD. + + repeat econstructor; eauto. + + do 2 (econstructor; eauto). + eapply has_loaded_default; eauto. + - (* Bcond *) repeat econstructor; eauto. + destruct ofin; intuition subst; + destruct b; eapply IHISTEP; eauto. Qed. Lemma normRTL_iblock_istep_correct tge sp ib rs0 m0 rs1 m1 ofin: |