diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-02-19 16:24:28 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-02-19 16:24:28 +0100 |
| commit | e51ffb6c1d9411515facc5e97a4e8dba5d8b55ab (patch) | |
| tree | 80a7fc8212d28712365082e1a2a2d0fa28cedad3 /backend/Constpropproof.v | |
| parent | c130f4936bad11fd6dab3a5d142b870d2a5f650c (diff) | |
| parent | b0eb1dfc9fd7b15c556c49101390d882b0f00f8a (diff) | |
| download | compcert-e51ffb6c1d9411515facc5e97a4e8dba5d8b55ab.tar.gz compcert-e51ffb6c1d9411515facc5e97a4e8dba5d8b55ab.zip | |
Merge branch 'master' into no-shell
Diffstat (limited to 'backend/Constpropproof.v')
| -rw-r--r-- | backend/Constpropproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index 98e6e577..450050de 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -277,11 +277,11 @@ Proof. + simpl in H. assert (V: vmatch bc (rs#r1) (Ptr (Gl symb n1))) by (rewrite <- e1; apply MATCH). exploit vmatch_ptr_gl'; eauto. intros [A | [b [A B]]]. * simpl in H; rewrite A in H; inv H. - * simpl; rewrite volatile_load_global_charact. exists b; split; congruence. + * simpl; rewrite volatile_load_global_charact; simpl. exists b; split; congruence. + simpl in H. assert (V: vmatch bc (rs#r1) (Ptr (Gl symb n1))) by (rewrite <- e1; apply MATCH). exploit vmatch_ptr_gl'; eauto. intros [A | [b [A B]]]. * simpl in H; rewrite A in H; inv H. - * simpl; rewrite volatile_store_global_charact. exists b; split; congruence. + * simpl; rewrite volatile_store_global_charact; simpl. exists b; split; congruence. + inv H. exploit annot_strength_reduction_correct; eauto. intros [eargs' [A B]]. rewrite <- B. econstructor; eauto. Qed. |