From a82c9c0e4a0b8e37c9c3ea5ae99714982563606f Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 14 Jan 2012 14:23:26 +0000 Subject: Merge of the nonstrict-ops branch: - Most RTL operators now evaluate to Some Vundef instead of None when undefined behavior occurs. - More aggressive instruction selection. - "Bertotization" of pattern-matchings now implemented by a proper preprocessor. - Cast optimization moved to cfrontend/Cminorgen; removed backend/CastOptim. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1790 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/Asmgenproof.v | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'arm/Asmgenproof.v') diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index 48f265b..a888aae 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -791,10 +791,9 @@ Proof. exists m'; split; auto. exists rs'; split. simpl. eexact P. assert (agree (Regmap.set res v ms) sp rs'). - apply agree_set_mreg with rs; auto. congruence. - auto with ppcgen. + apply agree_set_mreg with rs; auto. eapply Val.lessdef_trans; eauto. assert (agree (Regmap.set res v (undef_temps ms)) sp rs'). - apply agree_set_undef_mreg with rs; auto. congruence. + apply agree_set_undef_mreg with rs; auto. eapply Val.lessdef_trans; eauto. auto with ppcgen. destruct op; assumption. Qed. @@ -1086,7 +1085,8 @@ Proof. exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros A. exploit transl_cond_correct. eauto. eauto. - intros [rs2 [EX [RES OTH]]]. + instantiate (1 := rs). instantiate (1 := m'). unfold PregEq.t. rewrite A. + intros [rs2 [EX [RES OTH]]]. inv AT. simpl in H5. generalize (functions_transl _ _ H4); intro FN. generalize (functions_transl_no_overflow _ _ H4); intro NOOV. @@ -1120,7 +1120,8 @@ Proof. intro WTI. inv WTI. exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros A. - exploit transl_cond_correct. eauto. eauto. + exploit transl_cond_correct. eauto. + instantiate (1 := rs). instantiate (1 := m'). unfold PregEq.t. rewrite A. intros [rs2 [EX [RES OTH]]]. left; eapply exec_straight_steps; eauto with coqlib. exists m'; split; auto. -- cgit v1.2.3