From 0899bd69f402eb68d55297afe7131dbc539b693a Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 8 Jan 2013 09:46:59 +0000 Subject: Avoid generating some obviously useless casts. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2093 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/SimplLocalsproof.v | 23 ++++++++++++++++++++++- 1 file changed, 22 insertions(+), 1 deletion(-) (limited to 'cfrontend/SimplLocalsproof.v') diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index e08ae49b..f58a2130 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -340,6 +340,27 @@ Proof. destruct a as [id ty]. inv H. constructor; auto. Qed. +(** Correctness of [make_cast] *) + +Lemma make_cast_correct: + forall e le m a v1 tto v2, + eval_expr tge e le m a v1 -> + sem_cast v1 (typeof a) tto = Some v2 -> + eval_expr tge e le m (make_cast a tto) v2. +Proof. + intros. + assert (DFL: eval_expr tge e le m (Ecast a tto) v2). + econstructor; eauto. + unfold sem_cast, make_cast in *. + destruct (classify_cast (typeof a) tto); auto. + destruct v1; inv H0; auto. + destruct sz2; auto. destruct v1; inv H0; auto. + destruct sz2; auto. destruct v1; inv H0; auto. + destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H0; auto. + destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H0; auto. + inv H0; auto. +Qed. + (** Preservation by assignment to lifted variable. *) Lemma match_envs_assign_lifted: @@ -2009,7 +2030,7 @@ Proof. inv H. (* local variable *) econstructor; split. - apply plus_one. econstructor. econstructor. eexact A. rewrite typeof_simpl_expr. eexact C. + apply plus_one. econstructor. eapply make_cast_correct. eexact A. rewrite typeof_simpl_expr. eexact C. econstructor; eauto with compat. eapply match_envs_assign_lifted; eauto. eapply cast_val_is_casted; eauto. eapply match_cont_assign_loc; eauto. exploit me_range; eauto. omega. -- cgit