diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-01-23 13:33:33 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-01-23 13:33:33 +0100 |
| commit | b5b681b7b55abb18165eaa907b04aefb9b0fddde (patch) | |
| tree | 9c0a7df4b20ede85b54fe5c4e5d326fbf30a0013 /backend | |
| parent | 12803784f2753863985d1030999469c18e01e0f1 (diff) | |
| parent | f00b70b6a17fdfb4e8606df891f6becc8102ef12 (diff) | |
| download | compcert-b5b681b7b55abb18165eaa907b04aefb9b0fddde.tar.gz compcert-b5b681b7b55abb18165eaa907b04aefb9b0fddde.zip | |
Merge branch 'master' into dwarf
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/Constpropproof.v | 4 | ||||
| -rw-r--r-- | backend/Unusedglobproof.v | 6 | ||||
| -rw-r--r-- | backend/ValueAnalysis.v | 2 |
3 files changed, 6 insertions, 6 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. diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v index 5be9344f..fbf43866 100644 --- a/backend/Unusedglobproof.v +++ b/backend/Unusedglobproof.v @@ -530,7 +530,7 @@ Proof. { unfold tge; rewrite Genv.globalenv_public. unfold transform_program in TRANSF. rewrite USED_GLOBALS in TRANSF. inversion TRANSF. auto. } split; [|split;[|split]]; intros. - + unfold Genv.public_symbol; rewrite E1, E2. + + simpl; unfold Genv.public_symbol; rewrite E1, E2. destruct (Genv.find_symbol tge id) as [b'|] eqn:TFS. exploit symbols_inject_3; eauto. intros (b & FS & INJ). rewrite FS. auto. destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto. @@ -538,13 +538,13 @@ Proof. exploit symbols_inject_2; eauto. apply kept_public; auto. intros (b' & TFS' & INJ). congruence. + eapply symbols_inject_1; eauto. - + unfold Genv.public_symbol in H0. + + simpl in *; unfold Genv.public_symbol in H0. destruct (Genv.find_symbol ge id) as [b|] eqn:FS; try discriminate. rewrite E1 in H0. destruct (in_dec ident_eq id (prog_public p)); try discriminate. inv H1. exploit symbols_inject_2; eauto. apply kept_public; auto. intros (b' & A & B); exists b'; auto. - + unfold block_is_volatile. + + simpl. unfold Genv.block_is_volatile. destruct (Genv.find_var_info ge b1) as [gv|] eqn:V1. exploit var_info_inject; eauto. intros [A B]. rewrite A. auto. destruct (Genv.find_var_info tge b2) as [gv|] eqn:V2; auto. diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index b446e101..4249a8da 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -1273,7 +1273,7 @@ Proof. inv H2. * (* true volatile access *) assert (V: vmatch bc v0 (Ifptr Glob)). - { inv H4; constructor. econstructor. eapply GE; eauto. } + { inv H4; simpl in *; constructor. econstructor. eapply GE; eauto. } destruct (va_strict tt). apply vmatch_lub_r. apply vnormalize_sound. auto. apply vnormalize_sound. eapply vmatch_ge; eauto. constructor. constructor. * (* normal memory access *) |