diff options
Diffstat (limited to 'backend/CSEproof.v')
| -rw-r--r-- | backend/CSEproof.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 74e3ceca..c24fa69b 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -493,10 +493,10 @@ Lemma store_normalized_range_sound: Val.lessdef (Val.load_result chunk v) v. Proof. intros. destruct chunk; simpl in *; destruct v; auto. -- inv H. rewrite is_sgn_sign_ext in H3 by omega. rewrite H3; auto. -- inv H. rewrite is_uns_zero_ext in H3 by omega. rewrite H3; auto. -- inv H. rewrite is_sgn_sign_ext in H3 by omega. rewrite H3; auto. -- inv H. rewrite is_uns_zero_ext in H3 by omega. rewrite H3; auto. +- inv H. rewrite is_sgn_sign_ext in H4 by omega. rewrite H4; auto. +- inv H. rewrite is_uns_zero_ext in H4 by omega. rewrite H4; auto. +- inv H. rewrite is_sgn_sign_ext in H4 by omega. rewrite H4; auto. +- inv H. rewrite is_uns_zero_ext in H4 by omega. rewrite H4; auto. Qed. Lemma add_store_result_hold: @@ -696,7 +696,7 @@ Proof. rs#r = Vptr b o -> aaddr approx r = Stk i -> b = sp /\ i = o). { intros until i. unfold aaddr; subst approx. intros. - specialize (H5 r). rewrite H6 in H5. rewrite match_aptr_of_aval in H5. + specialize (H5 r). rewrite H6 in H5. apply match_aptr_of_aval in H5. rewrite H10 in H5. inv H5. split; auto. eapply bc_stack; eauto. } exploit (A rsrc); eauto. intros [P Q]. |