Do not use Format for faster printing of RTL, XTL, LTL, Mach

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2337 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

5 files changed, 128 insertions, 136 deletions

diff --git a/backend/PrintLTL.ml b/backend/PrintLTL.ml
index 702c213..52e5130 100644
--- a/backend/PrintLTL.ml
+++ b/backend/PrintLTL.ml
@@ -12,7 +12,7 @@
 
 (** Pretty-printers for RTL code *)
 
-open Format
+open Printf
 open Camlcoq
 open Datatypes
 open Maps
@@ -57,73 +57,72 @@ let ros pp = function
   | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s)
 
 let print_succ pp s dfl =
-  let s = P.to_int32 s in
-  if s <> dfl then fprintf pp "goto %ld" s
+  let s = P.to_int s in
+  if s <> dfl then fprintf pp "goto %d" s
 
 let print_instruction pp succ = function
   | Lop(op, args, res) ->
-      fprintf pp "%a = %a;" mreg res (print_operation mreg) (op, args)
+      fprintf pp "%a = %a" mreg res (print_operation mreg) (op, args)
   | Lload(chunk, addr, args, dst) ->
-      fprintf pp "%a = %s[%a];"
+      fprintf pp "%a = %s[%a]"
          mreg dst (name_of_chunk chunk) (print_addressing mreg) (addr, args)
   | Lgetstack(sl, ofs, ty, dst) ->
-      fprintf pp "%a = %a;" mreg dst slot (sl, ofs, ty)
+      fprintf pp "%a = %a" mreg dst slot (sl, ofs, ty)
   | Lsetstack(src, sl, ofs, ty) ->
-      fprintf pp "%a = %a;" slot (sl, ofs, ty) mreg src
+      fprintf pp "%a = %a" slot (sl, ofs, ty) mreg src
   | Lstore(chunk, addr, args, src) ->
-      fprintf pp "%s[%a] = %a;"
+      fprintf pp "%s[%a] = %a"
          (name_of_chunk chunk) (print_addressing mreg) (addr, args) mreg src
   | Lcall(sg, fn) ->
-      fprintf pp "call %a;" ros fn
+      fprintf pp "call %a" ros fn
   | Ltailcall(sg, fn) ->
-      fprintf pp "tailcall %a;" ros fn
+      fprintf pp "tailcall %a" ros fn
   | Lbuiltin(ef, args, res) ->
-      fprintf pp "%a = builtin %s(%a);"
+      fprintf pp "%a = %s(%a)"
         mregs res (name_of_external ef) mregs args
   | Lannot(ef, args) ->
-      fprintf pp "builtin %s(%a);"
+      fprintf pp "%s(%a)"
         (name_of_external ef) locs args
   | Lbranch s ->
       print_succ pp s succ
   | Lcond(cond, args, s1, s2) ->
-      fprintf pp "if (%a) goto %ld else goto %ld"
+      fprintf pp "if (%a) goto %d else goto %d"
         (print_condition mreg) (cond, args)
-        (P.to_int32 s1) (P.to_int32 s2)
+        (P.to_int s1) (P.to_int s2)
   | Ljumptable(arg, tbl) ->
       let tbl = Array.of_list tbl in
-      fprintf pp "@[<v 2>jumptable (%a)" mreg arg;
+      fprintf pp "jumptable (%a)" mreg arg;
       for i = 0 to Array.length tbl - 1 do
-        fprintf pp "@ case %d: goto %ld" i (P.to_int32 tbl.(i))
-      done;
-      fprintf pp "@]"
+        fprintf pp "\n\t\tcase %d: goto %d" i (P.to_int tbl.(i))
+      done
   | Lreturn ->
       fprintf pp "return"
 
 let rec print_instructions pp succ = function
   | [] -> ()
-  | [i] -> print_instruction pp succ i
+  | [i] ->  print_instruction pp succ i
   | i :: il ->
       print_instruction pp succ i;
-      fprintf pp "@ ";
+      fprintf pp "; ";
       print_instructions pp succ il
 
 let print_block pp (pc, blk) =
-  fprintf pp "%5ld: @[<hov 0>" pc;
-  print_instructions pp (Int32.pred pc) blk;
-  fprintf pp "@]@ "
+  fprintf pp "%5d:\t" pc;
+  print_instructions pp (pc - 1) blk;
+  fprintf pp "\n"
 
 let print_function pp id f =
-  fprintf pp "@[<v 2>%s() {@ " (extern_atom id);
+  fprintf pp "%s() {\n" (extern_atom id);
   let instrs =
     List.sort
       (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1)
       (List.rev_map
-        (fun (pc, i) -> (P.to_int32 pc, i))
+        (fun (pc, i) -> (P.to_int pc, i))
         (PTree.elements f.fn_code)) in
-  print_succ pp f.fn_entrypoint 
-    (match instrs with (pc1, _) :: _ -> pc1 | [] -> -1l);
+  print_succ pp f.fn_entrypoint
+    (match instrs with (pc1, _) :: _ -> pc1 | [] -> -1);
   List.iter (print_block pp) instrs;
-  fprintf pp "@;<0 -2>}@]@."
+  fprintf pp "}\n\n"
 
 let print_globdef pp (id, gd) =
   match gd with
@@ -140,6 +139,5 @@ let print_if prog =
   | None -> ()
   | Some f ->
       let oc = open_out f in
-      let pp = formatter_of_out_channel oc in
-      print_program pp prog;
+      print_program oc prog;
       close_out oc
diff --git a/backend/PrintMach.ml b/backend/PrintMach.ml
index e7cb947..b356ca9 100644
--- a/backend/PrintMach.ml
+++ b/backend/PrintMach.ml
@@ -12,7 +12,7 @@
 
 (** Pretty-printer for Mach code *)
 
-open Format
+open Printf
 open Camlcoq
 open Datatypes
 open Maps
@@ -50,57 +50,56 @@ let ros pp = function
 let print_instruction pp i =
   match i with
   | Mgetstack(ofs, ty, res) ->
-      fprintf pp "%a = stack(%ld, %s)@ "
+      fprintf pp "\t%a = stack(%ld, %s)\n"
               reg res (camlint_of_coqint ofs) (name_of_type ty)
   | Msetstack(arg, ofs, ty) ->
-      fprintf pp "stack(%ld, %s) = %a@ "
+      fprintf pp "\tstack(%ld, %s) = %a\n"
               (camlint_of_coqint ofs) (name_of_type ty) reg arg
   | Mgetparam(ofs, ty, res) ->
-      fprintf pp "%a = param(%ld, %s)@ "
+      fprintf pp "\t%a = param(%ld, %s)\n"
               reg res (camlint_of_coqint ofs) (name_of_type ty)
   | Mop(op, args, res) ->
-      fprintf pp "%a = %a@ "
+      fprintf pp "\t%a = %a\n"
          reg res (PrintOp.print_operation reg) (op, args)
   | Mload(chunk, addr, args, dst) ->
-      fprintf pp "%a = %s[%a]@ "
+      fprintf pp "\t%a = %s[%a]\n"
          reg dst (name_of_chunk chunk)
          (PrintOp.print_addressing reg) (addr, args)
   | Mstore(chunk, addr, args, src) ->
-      fprintf pp "%s[%a] = %a@ "
+      fprintf pp "\t%s[%a] = %a\n"
          (name_of_chunk chunk)
          (PrintOp.print_addressing reg) (addr, args)
          reg src
   | Mcall(sg, fn) ->
-      fprintf pp "call %a@ " ros fn
+      fprintf pp "\tcall %a\n" ros fn
   | Mtailcall(sg, fn) ->
-      fprintf pp "tailcall %a@ " ros fn
+      fprintf pp "\ttailcall %a\n" ros fn
   | Mbuiltin(ef, args, res) ->
-      fprintf pp "%a = builtin %s(%a)@ "
+      fprintf pp "\t%a = %s(%a)\n"
         regs res (name_of_external ef) regs args
   | Mannot(ef, args) ->
-      fprintf pp "%s(%a)@ " (name_of_external ef) annot_params args
+      fprintf pp "\t%s(%a)\n" (name_of_external ef) annot_params args
   | Mlabel lbl ->
-      fprintf pp "%ld:@ " (P.to_int32 lbl)
+      fprintf pp "%5d:" (P.to_int lbl)
   | Mgoto lbl ->
-      fprintf pp "goto %ld@ " (P.to_int32 lbl)
+      fprintf pp "\tgoto %d\n" (P.to_int lbl)
   | Mcond(cond, args, lbl) ->
-      fprintf pp "if (%a) goto %ld@ "
+      fprintf pp "\tif (%a) goto %d\n"
         (PrintOp.print_condition reg) (cond, args)
-        (P.to_int32 lbl)
+        (P.to_int lbl)
   | Mjumptable(arg, tbl) ->
       let tbl = Array.of_list tbl in
-      fprintf pp "@[<v 2>jumptable (%a)" reg arg;
+      fprintf pp "\tjumptable (%a)\n" reg arg;
       for i = 0 to Array.length tbl - 1 do
-        fprintf pp "@ case %d: goto %ld" i (P.to_int32 tbl.(i))
-      done;
-      fprintf pp "@]@ "
+        fprintf pp "\t\tcase %d: goto %d\n" i (P.to_int tbl.(i))
+      done
   | Mreturn ->
-      fprintf pp "return@ "
+      fprintf pp "\treturn\n"
 
 let print_function pp id f =
-  fprintf pp "@[<v 2>%s() {@ " (extern_atom id);
+  fprintf pp "%s() {\n" (extern_atom id);
   List.iter (print_instruction pp) f.fn_code;
-  fprintf pp "@;<0 -2>}@]@."
+  fprintf pp "}\n\n"
 
 let print_globdef pp (id, gd) =
   match gd with
@@ -117,6 +116,5 @@ let print_if prog =
   | None -> ()
   | Some f ->
       let oc = open_out f in
-      let pp = formatter_of_out_channel oc in
-      print_program pp prog;
+      print_program oc prog;
       close_out oc
diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml
index 0cdf505..429199e 100644
--- a/backend/PrintRTL.ml
+++ b/backend/PrintRTL.ml
@@ -12,7 +12,7 @@
 
 (** Pretty-printers for RTL code *)
 
-open Format
+open Printf
 open Camlcoq
 open Datatypes
 open Maps
@@ -25,7 +25,7 @@ open PrintOp
 (* Printing of RTL code *)
 
 let reg pp r =
-  fprintf pp "x%ld" (P.to_int32 r)
+  fprintf pp "x%d" (P.to_int r)
 
 let rec regs pp = function
   | [] -> ()
@@ -37,71 +37,70 @@ let ros pp = function
   | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s)
 
 let print_succ pp s dfl =
-  let s = P.to_int32 s in
-  if s <> dfl then fprintf pp "       goto %ld@ " s
+  let s = P.to_int s in
+  if s <> dfl then fprintf pp "\tgoto %d\n" s
 
 let print_instruction pp (pc, i) =
-  fprintf pp "%5ld: " pc;
+  fprintf pp "%5d:\t" pc;
   match i with
   | Inop s ->
-      let s = P.to_int32 s in
-      if s = Int32.pred pc
-      then fprintf pp "nop@ "
-      else fprintf pp "goto %ld@ " s
+      let s = P.to_int s in
+      if s = pc - 1
+      then fprintf pp "nop\n"
+      else fprintf pp "goto %d\n" s
   | Iop(op, args, res, s) ->
-      fprintf pp "%a = %a@ "
+      fprintf pp "%a = %a\n"
          reg res (PrintOp.print_operation reg) (op, args);
-      print_succ pp s (Int32.pred pc)
+      print_succ pp s (pc - 1)
   | Iload(chunk, addr, args, dst, s) ->
-      fprintf pp "%a = %s[%a]@ "
+      fprintf pp "%a = %s[%a]\n"
          reg dst (name_of_chunk chunk)
          (PrintOp.print_addressing reg) (addr, args);
-      print_succ pp s (Int32.pred pc)
+      print_succ pp s (pc - 1)
   | Istore(chunk, addr, args, src, s) ->
-      fprintf pp "%s[%a] = %a@ "
+      fprintf pp "%s[%a] = %a\n"
          (name_of_chunk chunk)
          (PrintOp.print_addressing reg) (addr, args)
          reg src;
-      print_succ pp s (Int32.pred pc)
+      print_succ pp s (pc - 1)
   | Icall(sg, fn, args, res, s) ->
-      fprintf pp "%a = %a(%a)@ "
+      fprintf pp "%a = %a(%a)\n"
         reg res ros fn regs args;
-      print_succ pp s (Int32.pred pc)
+      print_succ pp s (pc - 1)
   | Itailcall(sg, fn, args) ->
-      fprintf pp "tailcall %a(%a)@ "
+      fprintf pp "tailcall %a(%a)\n"
         ros fn regs args
   | Ibuiltin(ef, args, res, s) ->
-      fprintf pp "%a = builtin %s(%a)@ "
+      fprintf pp "%a = %s(%a)\n"
         reg res (name_of_external ef) regs args;
-      print_succ pp s (Int32.pred pc)
+      print_succ pp s (pc - 1)
   | Icond(cond, args, s1, s2) ->
-      fprintf pp "if (%a) goto %ld else goto %ld@ "
+      fprintf pp "if (%a) goto %d else goto %d\n"
         (PrintOp.print_condition reg) (cond, args)
-        (P.to_int32 s1) (P.to_int32 s2)
+        (P.to_int s1) (P.to_int s2)
   | Ijumptable(arg, tbl) ->
       let tbl = Array.of_list tbl in
-      fprintf pp "@[<v 2>jumptable (%a)" reg arg;
+      fprintf pp "jumptable (%a)\n" reg arg;
       for i = 0 to Array.length tbl - 1 do
-        fprintf pp "@ case %d: goto %ld" i (P.to_int32 tbl.(i))
-      done;
-      fprintf pp "@]@ "
+        fprintf pp "\t\tcase %d: goto %d\n" i (P.to_int tbl.(i))
+      done
   | Ireturn None ->
-      fprintf pp "return@ "
+      fprintf pp "return\n"
   | Ireturn (Some arg) ->
-      fprintf pp "return %a@ " reg arg
+      fprintf pp "return %a\n" reg arg
 
 let print_function pp id f =
-  fprintf pp "@[<v 2>%s(%a) {@ " (extern_atom id) regs f.fn_params;
+  fprintf pp "%s(%a) {\n" (extern_atom id) regs f.fn_params;
   let instrs =
     List.sort
       (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1)
       (List.rev_map
-        (fun (pc, i) -> (P.to_int32 pc, i))
+        (fun (pc, i) -> (P.to_int pc, i))
         (PTree.elements f.fn_code)) in
   print_succ pp f.fn_entrypoint 
-    (match instrs with (pc1, _) :: _ -> pc1 | [] -> -1l);
+    (match instrs with (pc1, _) :: _ -> pc1 | [] -> -1);
   List.iter (print_instruction pp) instrs;
-  fprintf pp "@;<0 -2>}@]@."
+  fprintf pp "}\n\n"
 
 let print_globdef pp (id, gd) =
   match gd with
@@ -116,8 +115,7 @@ let print_if optdest prog =
   | None -> ()
   | Some f ->
       let oc = open_out f in
-      let pp = formatter_of_out_channel oc in
-      print_program pp prog;
+      print_program oc prog;
       close_out oc
 
 let destination_rtl : string option ref = ref None
diff --git a/backend/PrintXTL.ml b/backend/PrintXTL.ml
index 258baba..ff45809 100644
--- a/backend/PrintXTL.ml
+++ b/backend/PrintXTL.ml
@@ -12,7 +12,7 @@
 
 (** Pretty-printer for XTL *)
 
-open Format
+open Printf
 open Camlcoq
 open Datatypes
 open Maps
@@ -49,8 +49,8 @@ let current_liveness = ref (None: VSet.t PMap.t option)
 
 let reg pp r ty =
   match !current_alloc with
-  | None -> fprintf pp "x%ld" (P.to_int32 r)
-  | Some alloc -> fprintf pp "x%ld{%a}" (P.to_int32 r) loc (alloc (V(r, ty)))
+  | None -> fprintf pp "x%d" (P.to_int r)
+  | Some alloc -> fprintf pp "x%d{%a}" (P.to_int r) loc (alloc (V(r, ty)))
 
 let var pp = function
   | V(r, ty) -> reg pp r ty
@@ -66,53 +66,52 @@ let ros pp = function
   | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s)
 
 let liveset pp lv =
-  fprintf pp "@[<hov 2>{";
-  VSet.iter (function V(r, ty) -> fprintf pp "@ x%ld" (P.to_int32 r)
+  fprintf pp "{";
+  VSet.iter (function V(r, ty) -> fprintf pp " x%d" (P.to_int r)
                     | L l -> ())
     lv;                  
-  fprintf pp " }@]"
+  fprintf pp " }"
 
 let print_succ pp s dfl =
-  let s = P.to_int32 s in
-  if s <> dfl then fprintf pp "goto %ld" s
+  let s = P.to_int s in
+  if s <> dfl then fprintf pp "goto %d" s
 
 let print_instruction pp succ = function
   | Xmove(src, dst) ->
-      fprintf pp "%a = %a;" var dst var src
+      fprintf pp "%a = %a" var dst var src
   | Xreload(src, dst) ->
-      fprintf pp "%a =r %a;" var dst var src
+      fprintf pp "%a =r %a" var dst var src
   | Xspill(src, dst) ->
-      fprintf pp "%a =s %a;" var dst var src
+      fprintf pp "%a =s %a" var dst var src
   | Xparmove(srcs, dsts, t1, t2) ->
-      fprintf pp "(%a) = (%a) using %a, %a;" vars dsts vars srcs var t1 var t2
+      fprintf pp "(%a) = (%a) using %a, %a" vars dsts vars srcs var t1 var t2
   | Xop(op, args, res) ->
-      fprintf pp "%a = %a;" var res (print_operation var) (op, args)
+      fprintf pp "%a = %a" var res (print_operation var) (op, args)
   | Xload(chunk, addr, args, dst) ->
-      fprintf pp "%a = %s[%a];"
+      fprintf pp "%a = %s[%a]"
          var dst (name_of_chunk chunk) (print_addressing var) (addr, args)
   | Xstore(chunk, addr, args, src) ->
-      fprintf pp "%s[%a] = %a;"
+      fprintf pp "%s[%a] = %a"
          (name_of_chunk chunk) (print_addressing var) (addr, args) var src
   | Xcall(sg, fn, args, res) ->
-      fprintf pp "%a = call %a(%a);" vars res ros fn vars args
+      fprintf pp "%a = call %a(%a)" vars res ros fn vars args
   | Xtailcall(sg, fn, args) ->
-      fprintf pp "tailcall %a(%a);" ros fn vars args
+      fprintf pp "tailcall %a(%a)" ros fn vars args
   | Xbuiltin(ef, args, res) ->
-      fprintf pp "%a = builtin %s(%a);"
+      fprintf pp "%a = %s(%a)"
         vars res (name_of_external ef) vars args
   | Xbranch s ->
       print_succ pp s succ
   | Xcond(cond, args, s1, s2) ->
-      fprintf pp "if (%a) goto %ld else goto %ld"
+      fprintf pp "if (%a) goto %d else goto %d"
         (print_condition var) (cond, args)
-        (P.to_int32 s1) (P.to_int32 s2)
+        (P.to_int s1) (P.to_int s2)
   | Xjumptable(arg, tbl) ->
       let tbl = Array.of_list tbl in
-      fprintf pp "@[<v 2>jumptable (%a)" var arg;
+      fprintf pp "jumptable (%a)" var arg;
       for i = 0 to Array.length tbl - 1 do
-        fprintf pp "@ case %d: goto %ld" i (P.to_int32 tbl.(i))
-      done;
-      fprintf pp "@]"
+        fprintf pp "\n\t\tcase %d: goto %d" i (P.to_int tbl.(i))
+      done
   | Xreturn args ->
       fprintf pp "return %a" vars args
 
@@ -121,31 +120,31 @@ let rec print_instructions pp succ = function
   | [i] -> print_instruction pp succ i
   | i :: il ->
       print_instruction pp succ i;
-      fprintf pp "@ ";
+      fprintf pp "; ";
       print_instructions pp succ il
 
 let print_block pp (pc, blk) =
-  fprintf pp "%5ld: @[<hov 0>" pc;
-  print_instructions pp (Int32.pred pc) blk;
-  fprintf pp "@]@ ";
+  fprintf pp "%5d:\t" pc;
+  print_instructions pp (pc - 1) blk;
+  fprintf pp "\n";
   match !current_liveness with
   | None -> ()
-  | Some liveness -> fprintf pp "%a@ " liveset (PMap.get (P.of_int32 pc) liveness)
+  | Some liveness -> fprintf pp "%a\n" liveset (PMap.get (P.of_int pc) liveness)
 
 let print_function pp ?alloc ?live f =
   current_alloc := alloc;
   current_liveness := live;
-  fprintf pp "@[<v 2>f() {@ ";
+  fprintf pp "f() {\n";
   let instrs =
     List.sort
       (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1)
       (List.map
-        (fun (pc, i) -> (P.to_int32 pc, i))
+        (fun (pc, i) -> (P.to_int pc, i))
         (PTree.elements f.fn_code)) in
   print_succ pp f.fn_entrypoint 
-    (match instrs with (pc1, _) :: _ -> pc1 | [] -> -1l);
+    (match instrs with (pc1, _) :: _ -> pc1 | [] -> -1);
   List.iter (print_block pp) instrs;
-  fprintf pp "@;<0 -2>}@]@.";
+  fprintf pp "}\n\n";
   current_alloc := None;
   current_liveness := None
 
diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml
index 3c56b43..8a3c05e 100644
--- a/backend/Regalloc.ml
+++ b/backend/Regalloc.ml
@@ -26,7 +26,7 @@
      End Repeat
 *)
 
-open Format
+open Printf
 open Clflags
 open Camlcoq
 open Datatypes
@@ -56,13 +56,13 @@ let is_two_address op args =
 (* For tracing *)
 
 let destination_alloctrace : string option ref = ref None
-let pp = ref std_formatter
+let pp = ref stdout
 
 let init_trace () =
-  if !option_dalloctrace && !pp == std_formatter then begin
+  if !option_dalloctrace && !pp == stdout then begin
     match !destination_alloctrace with
     | None -> ()  (* should not happen *)
-    | Some f -> pp := formatter_of_out_channel (open_out f)
+    | Some f -> pp := open_out f
   end
 
 
@@ -428,13 +428,12 @@ let spill_costs f =
     (fun () blk -> charge_block blk)
     f.fn_code ();
   if !option_dalloctrace then begin
-    fprintf !pp "------------------ Unspillable variables --------------@ @.";
-    fprintf !pp "@[<hov 1>";
+    fprintf !pp "------------------ Unspillable variables --------------\n\n";
     PTree.fold
       (fun () r st ->
-        if st.cost = max_int then fprintf !pp "@ x%ld" (P.to_int32 r))
+        if st.cost = max_int then fprintf !pp "x%d " (P.to_int r))
       !costs ();
-    fprintf !pp "@]@ @."
+    fprintf !pp "\n\n"
   end;
   (* Result is cost function: pseudoreg -> stats *)
   get_stats
@@ -938,7 +937,7 @@ exception Timeout
 let rec first_round f liveness =
   let alloc = find_coloring f liveness in
   if !option_dalloctrace then begin
-    fprintf !pp "-------------- After initial register allocation@ @.";
+    fprintf !pp "-------------- After initial register allocation\n\n";
     PrintXTL.print_function !pp ~alloc: alloc ~live: liveness f
   end;
   let ts = tospill_function f alloc in
@@ -950,7 +949,7 @@ and more_rounds f ts count =
   let liveness = liveness_analysis f' in
   let alloc = find_coloring f' liveness in
   if !option_dalloctrace then begin
-    fprintf !pp "-------------- After register allocation (round %d)@ @." count;
+    fprintf !pp "-------------- After register allocation (round %d)\n\n" count;
     PrintXTL.print_function !pp ~alloc: alloc ~live: liveness f'
   end;
   let ts' = tospill_function f' alloc in
@@ -958,9 +957,9 @@ and more_rounds f ts count =
   then success f' alloc
   else begin
     if !option_dalloctrace then begin
-      fprintf !pp "--- Remain to be spilled:@ @.";
+      fprintf !pp "--- Remain to be spilled:\n";
       VSet.iter (fun v -> fprintf !pp "%a " PrintXTL.var v) ts';
-      fprintf !pp "@ @."
+      fprintf !pp "\n\n"
     end;      
     more_rounds f (VSet.union ts ts') (count + 1)
   end
@@ -968,7 +967,7 @@ and more_rounds f ts count =
 and success f alloc =
   let f' = transl_function f alloc in
   if !option_dalloctrace then begin
-    fprintf !pp "-------------- Candidate allocation@ @.";
+    fprintf !pp "-------------- Candidate allocation\n\n";
     PrintLTL.print_function !pp P.one f'
   end;
   f'
@@ -987,12 +986,12 @@ let regalloc f =
       let liveness = liveness_analysis f2 in
       let f3 = dead_code_elimination f2 liveness in
       if !option_dalloctrace then begin
-        fprintf !pp "-------------- Initial XTL@ @.";
+        fprintf !pp "-------------- Initial XTL\n\n";
         PrintXTL.print_function !pp f3
       end;
       try
         OK(first_round f3 liveness)
-      with 
+      with
       | Timeout ->
           Error(msg (coqstring_of_camlstring "Spilling fails to converge"))
       | Type_error_at pc ->