Added option to dump preprocessed source code.

The new option -dprepro allows it to keep the preprocessed source code files.

2 files changed, 13 insertions, 4 deletions

diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index b67fd638..394dc448 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -33,6 +33,7 @@ let option_faligncondbranchs = ref 0
 let option_finline_asm = ref false
 let option_mthumb = ref (Configuration.model = "armv7m")
 let option_Osize = ref false
+let option_dprepro = ref false
 let option_dparse = ref false
 let option_dcmedium = ref false
 let option_dclight = ref false
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 352cbe41..78d141c1 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -282,18 +282,23 @@ let process_c_file sourcename =
     preprocess sourcename (output_filename_default "-");
     ""
   end else begin
-    let preproname = Filename.temp_file "compcert" ".i" in
+    let preproname = if !option_dprepro then 
+      output_filename sourcename ".c" ".i"
+    else
+      Filename.temp_file "compcert" ".i" in
     preprocess sourcename preproname;
     if !option_interp then begin
       Machine.config := Machine.compcert_interpreter !Machine.config;
       let csyntax,_ = parse_c_file sourcename preproname in
-      safe_remove preproname;
+      if not !option_dprepro then
+        safe_remove preproname;
       Interp.execute csyntax;
       ""
     end else if !option_S then begin
       compile_c_file sourcename preproname
                      (output_filename ~final:true sourcename ".c" ".s");
-      safe_remove preproname;
+      if not !option_dprepro then
+        safe_remove preproname;
       ""
     end else begin
       let asmname =
@@ -301,7 +306,8 @@ let process_c_file sourcename =
         then output_filename sourcename ".c" ".s"
         else Filename.temp_file "compcert" ".s" in
       compile_c_file sourcename preproname asmname;
-      safe_remove preproname;
+      if not !option_dprepro then
+        safe_remove preproname;
       let objname = output_filename ~final: !option_c sourcename ".c" ".o" in
       assemble asmname objname;
       if not !option_dasm then safe_remove asmname;
@@ -480,6 +486,7 @@ Linking options:
   -T <file>      Use <file> as linker command file
   -Wl,<opt>      Pass option <opt> to the linker
 Tracing options:
+  -dprepro       Save C file after preprocessing in <file>.i
   -dparse        Save C file after parsing and elaboration in <file>.parse.c
   -dc            Save generated Compcert C in <file>.compcert.c
   -dclight       Save generated Clight in <file>.light.c
@@ -602,6 +609,7 @@ let cmdline_actions =
     end);
   Prefix "-Wl,", Self push_linker_arg;
 (* Tracing options *)
+  Exact "-dprepro", Set option_dprepro;
   Exact "-dparse", Set option_dparse;
   Exact "-dc", Set option_dcmedium;
   Exact "-dclight", Set option_dclight;