diff options
| -rw-r--r-- | Changelog | 3 | ||||
| -rw-r--r-- | arm/PrintAsm.ml | 1 | ||||
| -rw-r--r-- | backend/PrintAnnot.ml | 11 | ||||
| -rw-r--r-- | driver/Driver.ml | 34 | ||||
| -rw-r--r-- | ia32/PrintAsm.ml | 1 | ||||
| -rw-r--r-- | powerpc/PrintAsm.ml | 1 |
6 files changed, 47 insertions, 4 deletions
@@ -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 |