From 92cca153569e44cd11ba3d1b68c2708c0cc46899 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 28 Jul 2021 17:00:02 +0200 Subject: ci fix? --- scheduling/RTLtoBTLproof.v | 27 +++++++++------------------ 1 file changed, 9 insertions(+), 18 deletions(-) (limited to 'scheduling/RTLtoBTLproof.v') diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index 13ba5a29..0ca93bce 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -624,26 +624,17 @@ Proof. - (* mib_seq *) inv IS_EXPD; try discriminate. inv H; simpl in *; try congruence; - inv STEP; try_simplify_someHyps; eauto. - + (* Bnop is_rtl *) - intros; eapply match_strong_state_simu; eauto. - + (* Bop *) - intros; eapply match_strong_state_simu; eauto. - econstructor; eauto. + inv STEP; try_simplify_someHyps; + intros; eapply match_strong_state_simu; eauto; + econstructor; eauto. + { (* Bop *) erewrite eval_operation_preserved in H12. erewrite H12 in BTL_RUN; simpl in BTL_RUN; auto. - intros; rewrite <- symbols_preserved; trivial. - + (* Bload *) - intros; eapply match_strong_state_simu; eauto. - econstructor; eauto. - erewrite eval_addressing_preserved in H12. - erewrite H12, H13 in BTL_RUN; simpl in BTL_RUN; auto. - intros; rewrite <- symbols_preserved; trivial. - + (* Bstore *) - intros; eapply match_strong_state_simu; eauto. - econstructor; eauto. - erewrite eval_addressing_preserved in H12. - erewrite H12, H13 in BTL_RUN; simpl in BTL_RUN; auto. + intros; rewrite <- symbols_preserved; trivial. } + all: (* Bload / Bstore *) + erewrite eval_addressing_preserved in H12; + try erewrite H12 in BTL_RUN; try erewrite H13 in BTL_RUN; + simpl in BTL_RUN; try destruct trap; auto; intros; rewrite <- symbols_preserved; trivial. - (* mib_cond *) inv IS_EXPD; try discriminate. -- cgit