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

1 files changed, 12 insertions, 15 deletions

diff --git a/backend/PrintLTLin.ml b/backend/PrintLTLin.ml
index adff483..bb360eb 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