summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Changelog3
-rw-r--r--arm/PrintAsm.ml1
-rw-r--r--backend/PrintAnnot.ml11
-rw-r--r--driver/Driver.ml34
-rw-r--r--ia32/PrintAsm.ml1
-rw-r--r--powerpc/PrintAsm.ml1
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