diff options
author | Léo Gourdin <leo.gourdin@lilo.org> | 2021-07-28 17:00:02 +0200 |
---|---|---|
committer | Léo Gourdin <leo.gourdin@lilo.org> | 2021-07-28 17:00:02 +0200 |
commit | 92cca153569e44cd11ba3d1b68c2708c0cc46899 (patch) | |
tree | 990c58ee9a15db32a6c87a8135295092433beb72 /scheduling/RTLtoBTLproof.v | |
parent | 23569a795598f18cad851f1bda39dd1a2e630ded (diff) | |
download | compcert-kvx-92cca153569e44cd11ba3d1b68c2708c0cc46899.tar.gz compcert-kvx-92cca153569e44cd11ba3d1b68c2708c0cc46899.zip |
ci fix?
Diffstat (limited to 'scheduling/RTLtoBTLproof.v')
-rw-r--r-- | scheduling/RTLtoBTLproof.v | 27 |
1 files changed, 9 insertions, 18 deletions
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. |