4 files changed, 18 insertions, 13 deletions

diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml
index 0a927873..d623ab96 100644
--- a/cparser/Cprint.ml
+++ b/cparser/Cprint.ml
@@ -555,3 +555,13 @@ let program pp prog =
   fprintf pp "@[<v 0>";
   List.iter (globdecl pp) prog;
   fprintf pp "@]@."
+
+let destination : string option ref = ref None
+
+let print_if prog =
+  match !destination with
+  | None -> ()
+  | Some f ->
+    let oc = open_out f in
+    program (formatter_of_out_channel oc) prog;
+    close_out oc
diff --git a/cparser/Cprint.mli b/cparser/Cprint.mli
index fe71e4fe..be7ce029 100644
--- a/cparser/Cprint.mli
+++ b/cparser/Cprint.mli
@@ -33,3 +33,6 @@ val storage : Format.formatter -> C.storage -> unit
 val field : Format.formatter -> C.field -> unit
 val globdecl : Format.formatter -> C.globdecl -> unit
 val program : Format.formatter -> C.program -> unit
+
+val destination : string option ref
+val print_if : C.program -> unit
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 5afa0a76..b23a4e4f 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -76,7 +76,9 @@ let compile_c_file sourcename ifile ofile =
   (* Prepare to dump Clight, RTL, etc, if requested *)
   let set_dest dst opt ext =
     dst := if !opt then Some (output_filename sourcename ".c" ext)
-                   else None in
+      else None in
+  set_dest Cprint.destination option_dparse ".parsed.c";
+  set_dest PrintCsyntax.destination option_dcmedium ".compcert.c";
   set_dest PrintClight.destination option_dclight ".light.c";
   set_dest PrintCminor.destination option_dcminor ".cm";
   set_dest PrintRTL.destination option_drtl ".rtl";
diff --git a/driver/Frontend.ml b/driver/Frontend.ml
index b4b161b0..148d0f74 100644
--- a/driver/Frontend.ml
+++ b/driver/Frontend.ml
@@ -59,12 +59,7 @@ let parse_c_file sourcename ifile =
     | None -> exit 2
     | Some p -> p in
   (* Save C AST if requested *)
-  if !option_dparse then begin
-    let ofile = output_filename sourcename ".c" ".parsed.c" in
-    let oc = open_out ofile in
-    Cprint.program (Format.formatter_of_out_channel oc) ast;
-    close_out oc
-  end;
+  Cprint.print_if ast;
   (* Conversion to Csyntax *)
   let csyntax =
     match Timing.time "CompCert C generation" C2C.convertProgram ast with
@@ -72,12 +67,7 @@ let parse_c_file sourcename ifile =
     | Some p -> p in
   flush stderr;
   (* Save CompCert C AST if requested *)
-  if !option_dcmedium then begin
-    let ofile = output_filename sourcename ".c" ".compcert.c" in
-    let oc = open_out ofile in
-    PrintCsyntax.print_program (Format.formatter_of_out_channel oc) csyntax;
-    close_out oc
-  end;
+  PrintCsyntax.print_if csyntax;
   csyntax
 
 (* Add gnu preprocessor list *)