From 4af1682d04244bab9f793e00eb24090153a36a0f Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 28 Jul 2011 12:51:16 +0000 Subject: Added animation of the CompCert C semantics (ccomp -interp) test/regression: int main() so that interpretation works Revised once more implementation of __builtin_memcpy (to check for PPC & ARM) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1688 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- driver/Compiler.v | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'driver/Compiler.v') diff --git a/driver/Compiler.v b/driver/Compiler.v index a51cd8ff..37a187ee 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -24,6 +24,7 @@ Require Import Smallstep. Require Csyntax. Require Csem. Require Cstrategy. +Require Cexec. Require Clight. Require Csharpminor. Require Cminor. @@ -82,8 +83,8 @@ Require Reloadtyping. Require Stackingproof. Require Stackingtyping. Require Asmgenproof. + (** Pretty-printers (defined in Caml). *) -Parameter print_Csyntax: Csyntax.program -> unit. Parameter print_Clight: Clight.program -> unit. Parameter print_Cminor: Cminor.program -> unit. Parameter print_RTL: RTL.fundef -> unit. @@ -180,13 +181,13 @@ Definition transf_clight_program (p: Clight.program) : res Asm.program := Definition transf_c_program (p: Csyntax.program) : res Asm.program := OK p - @@ print print_Csyntax @@@ SimplExpr.transl_program @@@ transf_clight_program. -(** Force [Initializers] to be extracted as well. *) +(** Force [Initializers] and [Cexec] to be extracted as well. *) Definition transl_init := Initializers.transl_init. +Definition cexec_do_step := Cexec.do_step. (** The following lemmas help reason over compositions of passes. *) @@ -403,7 +404,7 @@ Theorem transf_cstrategy_program_correct: Proof. intros. assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics tp)). - revert H; unfold transf_c_program; simpl. rewrite print_identity. + revert H; unfold transf_c_program; simpl. caseEq (SimplExpr.transl_program p); simpl; try congruence; intros p0 EQ0. intros EQ1. eapply compose_forward_simulation. apply SimplExprproof.transl_program_correct. eauto. -- cgit