Recognize .i and .p source files as C sources not to be preprocessed.

Add CompCert version number and command line as comments in generated asm.


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

6 files changed, 47 insertions, 4 deletions

diff --git a/Changelog b/Changelog
index 8baf25f..eac8a4d 100644
--- a/Changelog
+++ b/Changelog
@@ -17,7 +17,8 @@
 - More tolerance for functions declared without a prototype
   (option -funprototyped, on by default).
 - Option -drtl.
-
+- Recognize source files with .i or .p extension as C sources that
+  should not be preprocessed.
 
 Release 2.1, 2013-10-28
 =======================
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 01b881f..66aa908 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -888,6 +888,7 @@ let print_globdef oc (name, gdef) =
 
 let print_program oc p =
 (*  fprintf oc "	.fpu	vfp\n"; *)
+  PrintAnnot.print_version_and_options oc comment;
   Hashtbl.clear filename_num;
   List.iter (print_globdef oc) p.prog_defs
 
diff --git a/backend/PrintAnnot.ml b/backend/PrintAnnot.ml
index 1ebb51f..d24635a 100644
--- a/backend/PrintAnnot.ml
+++ b/backend/PrintAnnot.ml
@@ -74,3 +74,14 @@ let print_annot_stmt print_preg sp_reg_name oc txt tmpl args =
 let print_annot_val print_preg oc txt args =
   print_annot_text print_preg "<internal error>" oc txt
     (List.map (fun r -> Reg r) args)
+
+(* Print CompCert version and command-line as asm comment *)
+
+let print_version_and_options oc comment =
+  fprintf oc "%s File generated by CompCert %s\n" comment Configuration.version;
+  fprintf oc "%s Command line:" comment;
+  for i = 1 to Array.length Sys.argv - 1 do
+    fprintf oc " %s" Sys.argv.(i)
+  done;
+  fprintf oc "\n"
+
diff --git a/driver/Driver.ml b/driver/Driver.ml
index c35ac1f..47061cd 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -102,8 +102,6 @@ let parse_c_file sourcename ifile =
     match Parse.preprocessed_file simplifs sourcename ifile with
     | None -> exit 2
     | Some p -> p in
-  (* Remove preprocessed file (always a temp file) *)
-  safe_remove ifile;
   (* Save C AST if requested *)
   if !option_dparse then begin
     let ofile = output_filename sourcename ".c" ".parsed.c" in
@@ -238,11 +236,13 @@ let process_c_file sourcename =
     preprocess sourcename preproname;
     if !option_interp then begin
       let csyntax = parse_c_file sourcename preproname in
+      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;
       ""
     end else begin
       let asmname =
@@ -250,6 +250,7 @@ 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;
       let objname = output_filename ~final: !option_c sourcename ".c" ".o" in
       assemble asmname objname;
       if not !option_dasm then safe_remove asmname;
@@ -257,6 +258,29 @@ let process_c_file sourcename =
     end
   end
 
+(* Processing of a .i / .p file (preprocessed C) *)
+
+let process_i_file sourcename =
+  if !option_interp then begin
+    let csyntax = parse_c_file sourcename sourcename in
+    Interp.execute csyntax;
+    ""
+  end else if !option_S then begin
+    compile_c_file sourcename sourcename
+                   (output_filename ~final:true sourcename ".c" ".s");
+    ""
+  end else begin
+    let asmname =
+      if !option_dasm
+      then output_filename sourcename ".c" ".s"
+      else Filename.temp_file "compcert" ".s" in
+    compile_c_file sourcename sourcename asmname;
+    let objname = output_filename ~final: !option_c sourcename ".c" ".o" in
+    assemble asmname objname;
+    if not !option_dasm then safe_remove asmname;
+    objname
+  end
+
 (* Processing of a .cm file *)
 
 let process_cminor_file sourcename =
@@ -375,9 +399,10 @@ let usage_string =
 Usage: ccomp [options] <source files>
 Recognized source files:
   .c             C source file
+  .i or .p       C source file that should not be preprocessed
   .cm            Cminor source file
   .s             Assembly file
-  .S             Assembly file, to be run through the preprocessor
+  .S             Assembly file that must be preprocessed
   .o             Object file
   .a             Library file
 Processing options:
@@ -480,6 +505,9 @@ let cmdline_actions =
   ".*\\.c$", Self (fun s ->
       push_action process_c_file s;
       incr num_source_files);
+  ".*\\.[ip]$", Self (fun s ->
+      push_action process_i_file s;
+      incr num_source_files);
   ".*\\.cm$", Self (fun s ->
       push_action process_cminor_file s;
       incr num_source_files);
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index 01034f1..79da85e 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -873,6 +873,7 @@ let print_globdef oc (name, gdef) =
   | Gvar v -> print_var oc name v
 
 let print_program oc p =
+  PrintAnnot.print_version_and_options oc comment;
   need_masks := false;
   indirect_symbols := StringSet.empty;
   Hashtbl.clear filename_num;
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index b9778c4..b90b9f2 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -1203,6 +1203,7 @@ let print_prologue oc =
 
 let print_program oc p =
   reset_file_line();
+  PrintAnnot.print_version_and_options oc comment;
   print_prologue oc;
   List.iter (print_globdef oc) p.prog_defs