diff options
Diffstat (limited to 'scheduling/RTLtoBTLproof.v')
| -rw-r--r-- | scheduling/RTLtoBTLproof.v | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index 0ca93bce..6ec32ffc 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -631,9 +631,13 @@ Proof. erewrite eval_operation_preserved in H12. erewrite H12 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; + (* Bload/Bstore *) + inv H12; [ idtac | destruct (eval_addressing) eqn:EVAL in LOAD;[ specialize (LOAD v) |] ]; + rename LOAD into MEMT. + 4: rename H12 into EVAL; rename H13 into MEMT. + all: + erewrite eval_addressing_preserved in EVAL; + try erewrite EVAL in BTL_RUN; try erewrite MEMT in BTL_RUN; simpl in BTL_RUN; try destruct trap; auto; intros; rewrite <- symbols_preserved; trivial. - (* mib_cond *) |