From 5fccbcb628c5282cf1b13077d5eeccf497d58c38 Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 14 Jul 2011 14:00:57 +0000 Subject: Fix treatment of function pointers at function calls in the CompCert C and Clight semantics git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1680 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cshmgenproof.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'cfrontend/Cshmgenproof.v') diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 457f0d1..49d3ff3 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -1525,11 +1525,10 @@ Proof. exploit transl_expr_correct; eauto. exploit transl_exprlist_correct; eauto. eapply transl_fundef_sig1; eauto. - rewrite H3. rewrite H. auto. + rewrite H3. auto. econstructor; eauto. econstructor; eauto. simpl. auto. - rewrite H3; rewrite H; eauto. eapply eval_exprlist_casted; eauto. (* seq *) -- cgit v1.2.3