aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Compiler.v
diff options
context:
space:
mode:
authorxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2011-05-08 08:39:30 +0000
committerxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2011-05-08 08:39:30 +0000
commitfb202a70ccc2872aa3849854c09810a6bee268e5 (patch)
tree1b2fa2f5fa1c7f84ff7589f778985a0db306d845 /driver/Compiler.v
parentc45fc2431ea70e0cb5a80e65d0ac99f91e94693e (diff)
downloadcompcert-fb202a70ccc2872aa3849854c09810a6bee268e5.tar.gz
compcert-fb202a70ccc2872aa3849854c09810a6bee268e5.zip
powerpc/PrintAsm.ml arm/PrintAsm.ml: updated (no label elimination).
Added -dmach option and corresponding printer for Mach code. CleanupLabelsproof.v: fixed for ARM Driver.ml: -E sends output to stdout; support for .s and .S source files. cparser/Elab.ml: spurious comment deleted. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1648 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'driver/Compiler.v')
-rw-r--r--driver/Compiler.v7
1 files changed, 4 insertions, 3 deletions
diff --git a/driver/Compiler.v b/driver/Compiler.v
index bde63089..d8810a4c 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -92,6 +92,7 @@ Parameter print_RTL_castopt: RTL.fundef -> unit.
Parameter print_RTL_constprop: RTL.fundef -> unit.
Parameter print_RTL_cse: RTL.fundef -> unit.
Parameter print_LTLin: LTLin.fundef -> unit.
+Parameter print_Mach: Mach.fundef -> unit.
Open Local Scope string_scope.
@@ -113,7 +114,7 @@ Notation "a @@ b" :=
(apply_total _ _ a b) (at level 50, left associativity).
Definition print {A: Type} (printer: A -> unit) (prog: A) : A :=
- match printer prog with tt => prog end.
+ let unused := printer prog in prog.
(** We define three translation functions for whole programs: one
starting with a C program, one with a Cminor program, one with an
@@ -149,6 +150,7 @@ Definition transf_rtl_fundef (f: RTL.fundef) : res Asm.fundef :=
@@ print print_LTLin
@@ Reload.transf_fundef
@@@ Stacking.transf_fundef
+ @@ print print_Mach
@@@ Asmgen.transf_fundef.
(* Here is the translation of a CminorSel function to an Asm function. *)
@@ -316,7 +318,7 @@ Proof.
Reloadtyping.program_typing_preserved
Stackingtyping.program_typing_preserved; intros.
- eapply Asmgenproof.transf_program_correct; eauto 6.
+ eapply Asmgenproof.transf_program_correct; eauto 8.
eapply Stackingproof.transf_program_correct; eauto 6.
eapply Reloadproof.transf_program_correct; eauto.
eapply CleanupLabelsproof.transf_program_correct; eauto.
@@ -341,7 +343,6 @@ Proof.
eapply transf_rtl_program_correct; eauto.
eapply RTLgenproof.transf_program_correct; eauto.
eapply Selectionproof.transf_program_correct; eauto.
- rewrite print_identity. auto.
Qed.
Theorem transf_c_program_correct: