From 7998ccfd709b97f1a2306df4570365d58a5bb4b5 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 12 Jan 2014 10:48:56 +0000 Subject: - Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4. - Revised printing of intermediate RTL code. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2403 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/PrintRTL.ml | 26 +++++--------------------- 1 file changed, 5 insertions(+), 21 deletions(-) (limited to 'backend/PrintRTL.ml') diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml index 137f65b..5c8347c 100644 --- a/backend/PrintRTL.ml +++ b/backend/PrintRTL.ml @@ -110,29 +110,13 @@ let print_globdef pp (id, gd) = let print_program pp (prog: RTL.program) = List.iter (print_globdef pp) prog.prog_defs -let print_if optdest prog = - match !optdest with +let destination : string option ref = ref None + +let print_if passno prog = + match !destination with | None -> () | Some f -> - let oc = open_out f in + let oc = open_out (f ^ "." ^ Z.to_string passno) in print_program oc prog; close_out oc -let destination_rtl : string option ref = ref None -let print_rtl = print_if destination_rtl - -let destination_tailcall : string option ref = ref None -let print_tailcall = print_if destination_tailcall - -let destination_inlining : string option ref = ref None -let print_inlining = print_if destination_inlining - -let destination_constprop : string option ref = ref None -let print_constprop = print_if destination_constprop - -let destination_cse : string option ref = ref None -let print_cse = print_if destination_cse - -let destination_deadcode : string option ref = ref None -let print_deadcode = print_if destination_deadcode - -- cgit v1.2.3