From 0d27eae0b07c7c46cb7d4e6d7b0b1145dbdab0c3 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 19 May 2013 07:57:29 +0000 Subject: Issue with simplification of nested ?: expressions of different types. (Ill-typed Clight/Cminor/RTL code was generated due to incorrect reuse of destination temporary.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2257 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/SimplExprproof.v | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) (limited to 'cfrontend/SimplExprproof.v') diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 150ed760..a2b8e615 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -192,8 +192,8 @@ Lemma tr_simple: match dst with | For_val => sl = nil /\ Csyntax.typeof r = typeof a /\ eval_expr tge e le m a v | For_effects => sl = nil - | For_set tyl t => - exists b, sl = do_set t tyl b + | For_set sd => + exists b, sl = do_set sd b /\ Csyntax.typeof r = typeof b /\ eval_expr tge e le m b v end) @@ -277,8 +277,8 @@ Lemma tr_simple_rvalue: match dst with | For_val => sl = nil /\ Csyntax.typeof r = typeof a /\ eval_expr tge e le m a v | For_effects => sl = nil - | For_set tyl t => - exists b, sl = do_set t tyl b + | For_set sd => + exists b, sl = do_set sd b /\ Csyntax.typeof r = typeof b /\ eval_expr tge e le m b v end. @@ -1063,9 +1063,9 @@ Proof. Qed. Lemma nolabel_do_set: - forall tmp tyl a, nolabel_list (do_set tmp tyl a). + forall sd a, nolabel_list (do_set sd a). Proof. - induction tyl; intros; simpl; split; auto; red; auto. + induction sd; intros; simpl; split; auto; red; auto. Qed. Lemma nolabel_final: @@ -1418,8 +1418,9 @@ Proof. apply push_seq. reflexivity. reflexivity. rewrite <- Kseqlist_app. eapply match_exprstates; eauto. - apply S. apply tr_paren_set with (a1 := dummy_expr); auto. econstructor; eauto. - apply tr_expr_monotone with tmp2; eauto. auto. auto. + apply S. apply tr_paren_set with (a1 := dummy_expr) (t := sd_temp sd); auto. + apply tr_paren_set with (a1 := a2) (t := sd_temp sd). + apply tr_expr_monotone with tmp2; eauto. auto. auto. auto. (* seqand false *) exploit tr_top_leftcontext; eauto. clear H9. intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [R S]]]]]]]]. @@ -1527,7 +1528,8 @@ Proof. apply push_seq. reflexivity. reflexivity. rewrite <- Kseqlist_app. eapply match_exprstates; eauto. - apply S. apply tr_paren_set with (a1 := dummy_expr); auto. econstructor; eauto. + apply S. apply tr_paren_set with (a1 := dummy_expr) (t := sd_temp sd); auto. + apply tr_paren_set with (a1 := a2) (t := sd_temp sd); auto. apply tr_expr_monotone with tmp2; eauto. auto. auto. (* condition *) exploit tr_top_leftcontext; eauto. clear H9. -- cgit