diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-07-28 12:51:16 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-07-28 12:51:16 +0000 |
commit | 4af1682d04244bab9f793e00eb24090153a36a0f (patch) | |
tree | a9a70d236c06a78aa9b607c6a41e09b80651aa51 /driver/Compiler.v | |
parent | d8d1bf1aa09373f64aa1b1e6cdfb914c23a910be (diff) | |
download | compcert-kvx-4af1682d04244bab9f793e00eb24090153a36a0f.tar.gz compcert-kvx-4af1682d04244bab9f793e00eb24090153a36a0f.zip |
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
Diffstat (limited to 'driver/Compiler.v')
-rw-r--r-- | driver/Compiler.v | 9 |
1 files changed, 5 insertions, 4 deletions
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. |