1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
open Clflags
open Commandline
open Driveraux
open Printf
(* Common frontend functions between clightgen and ccomp *)
(* From C to preprocessed C *)
let preprocess ifile ofile =
let output =
if ofile = "-" then None else Some ofile in
let cmd = List.concat [
Configuration.prepro;
["-D__COMPCERT__"];
(if !Clflags.use_standard_headers
then ["-I" ^ Filename.concat !Clflags.stdlib_path "include" ]
else []);
List.rev !prepro_options;
[ifile]
] in
let exc = command ?stdout:output cmd in
if exc <> 0 then begin
if ofile <> "-" then safe_remove ofile;
command_error "preprocessor" exc;
eprintf "Error during preprocessing.\n";
exit 2
end
(* From preprocessed C to Csyntax *)
let parse_c_file sourcename ifile =
Debug.init_compile_unit sourcename;
Sections.initialize();
(* Simplification options *)
let simplifs =
"b" (* blocks: mandatory *)
^ (if !option_fstruct_passing then "s" else "")
^ (if !option_fbitfields then "f" else "")
^ (if !option_fpacked_structs then "p" else "")
in
(* Parsing and production of a simplified C AST *)
let ast =
match Parse.preprocessed_file simplifs sourcename ifile with
| 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;
(* Conversion to Csyntax *)
let csyntax =
match Timing.time "CompCert C generation" C2C.convertProgram ast with
| None -> exit 2
| 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;
csyntax
(* Add gnu preprocessor list *)
let gnu_prepro_opt_key key s =
if gnu_option s then
prepro_options := s::key::!prepro_options
(* Add gnu preprocessor option *)
let gnu_prepro_opt s =
if gnu_option s then
prepro_options := s::!prepro_options
(* Add gnu preprocessor option s and the implict -E *)
let gnu_prepro_opt_e s =
if gnu_option s then begin
prepro_options := s :: !prepro_options;
option_E := true
end
let prepro_actions = [
(* Preprocessing options *)
Exact "-I", String(fun s -> prepro_options := s :: "-I" :: !prepro_options;
assembler_options := s :: "-I" :: !assembler_options);
Prefix "-I", Self(fun s -> prepro_options := s :: !prepro_options;
assembler_options := s :: !assembler_options);
Exact "-D", String(fun s -> prepro_options := s :: "-D" :: !prepro_options);
Prefix "-D", Self(fun s -> prepro_options := s :: !prepro_options);
Exact "-U", String(fun s -> prepro_options := s :: "-U" :: !prepro_options);
Prefix "-U", Self(fun s -> prepro_options := s :: !prepro_options);
Prefix "-Wp,", Self (fun s ->
prepro_options := List.rev_append (explode_comma_option s) !prepro_options);
Exact "-Xpreprocessor", String (fun s ->
prepro_options := s :: !prepro_options);
Exact "-include", String (fun s -> prepro_options := s :: "-include" :: !prepro_options);
Exact "-M", Self gnu_prepro_opt_e;
Exact "-MM", Self gnu_prepro_opt_e;
Exact "-MF", String (gnu_prepro_opt_key "-MF");
Exact "-MG", Self gnu_prepro_opt;
Exact "-MP", Self gnu_prepro_opt;
Exact "-MT", String (gnu_prepro_opt_key "-MT");
Exact "-MQ", String (gnu_prepro_opt_key "-MQ");
Exact "-nostdinc", Self (fun s -> gnu_prepro_opt s; use_standard_headers := false);
Exact "-imacros", String (gnu_prepro_opt_key "-imacros");
Exact "-idirafter", String (gnu_prepro_opt_key "-idirafter");
Exact "-isystem", String (gnu_prepro_opt_key "-isystem");
Exact "-iquote", String (gnu_prepro_opt_key "-iquore");
Exact "-P", Self gnu_prepro_opt;
Exact "-C", Self gnu_prepro_opt;
Exact "-CC", Self gnu_prepro_opt;]
let prepro_help = "Preprocessing options:\n\
\ -I<dir> Add <dir> to search path for #include files\n\
\ -include <file> Process <file> as if #include \"<file>\" appears at the first\n\
\ line of the primary source file.\n\
\ -D<symb>=<val> Define preprocessor symbol\n\
\ -U<symb> Undefine preprocessor symbol\n\
\ -Wp,<opt> Pass option <opt> to the preprocessor\n\
\ -Xpreprocessor <opt> Pass option <opt> to the preprocessor\n\
\ -M (GCC only) Ouput a rule suitable for make describing the\n\
\ dependencies of the main source file\n\
\ -MM (GCC only) Like -M but do not mention system header files\n\
\ -MF <file> (GCC only) Specifies file <file> as output file for -M or -MM\n\
\ -MG (GCC only) Assumes missing header files are generated for -M\n\
\ -MP (GCC only) Add a phony target for each dependency other than\n\
\ the main file\n\
\ -MT <target> (GCC only) Change the target of the rule emitted by dependency\n\
\ generation\n\
\ -MQ <target> (GCC only) Like -MT but quotes <target>\n\
\ -nostdinc (GCC only) Do not search the standard system directories for\n\
\ header files\n\
\ -imacros <file> (GCC only) Like -include but throws output produced by\n\
\ preprocessing of <file> away\n\
\ -idirafter <dir> (GCC only) Search <dir> for header files after all directories\n\
\ specified with -I and the standard system directories\n\
\ -isystem <dir> (GCC only) Search <dir> for header files after all directories\n\
\
\ specified by -I but before the standard system directories\n\
\ -iquote <dir> (GCC only) Like -isystem but only for headers included with\n\
\ quotes\n\
\ -P (GCC only) Do not generate linemarkers\n\
\ -C (GCC only) Do not discard comments\n\
\ -CC (GCC only) Do not discard comments, including during macro\n\
\ expansion\n"
|
