From 0053b1aa1d26da5d1f995a603b127daf799c2da9 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 21 May 2012 16:26:30 +0000
Subject: Merge of the newmem branch: - Revised memory model with Max and Cur
 permissions, but without bounds - Constant propagation of 'const' globals -
 Function inlining at RTL level - (Unprovable) elimination of unreferenced
 static definitions

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1899 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/PrintLTLin.ml | 27 ++++++++++++---------------
 1 file changed, 12 insertions(+), 15 deletions(-)

(limited to 'backend/PrintLTLin.ml')

diff --git a/backend/PrintLTLin.ml b/backend/PrintLTLin.ml
index adff4834..bb360eb3 100644
--- a/backend/PrintLTLin.ml
+++ b/backend/PrintLTLin.ml
@@ -90,29 +90,26 @@ let print_instruction pp i =
   | Lreturn (Some arg) ->
       fprintf pp "return %a@ " reg arg
 
-let print_function pp f =
-  fprintf pp "@[<v 2>f(%a) {@ " regs f.fn_params;
+let print_function pp id f =
+  fprintf pp "@[<v 2>%s(%a) {@ " (extern_atom id) regs f.fn_params;
   List.iter (print_instruction pp) f.fn_code;
   fprintf pp "@;<0 -2>}@]@."
 
-let print_fundef pp fd =
+let print_fundef pp (id, fd) =
   match fd with
-  | Internal f -> print_function pp f
+  | Internal f -> print_function pp id f
   | External _ -> ()
 
+let print_program pp prog =
+  List.iter (print_fundef pp) prog.prog_funct
+
 let destination : string option ref = ref None
-let currpp : formatter option ref = ref None
 
-let print_if fd =
+let print_if prog =
   match !destination with
   | None -> ()
   | Some f ->
-      let pp =
-        match !currpp with
-        | Some pp -> pp
-        | None ->
-            let oc = open_out f in
-            let pp = formatter_of_out_channel oc in
-            currpp := Some pp;
-            pp
-      in print_fundef pp fd
+      let oc = open_out f in
+      let pp = formatter_of_out_channel oc in
+      print_program pp prog;
+      close_out oc
-- 
cgit