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
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
|
.\" -*- nroff -*-
.TH CCOMP "1" "February 5, 2015" "CompCert 2.4" "User Commands"
.SH NAME
ccomp \- CompCert C compiler
.SH SYNOPSIS
.B ccomp
[\fIOPTION\fR]... \fISOURCE-FILE\fR...
.SH DESCRIPTION
CompCert, invoked as \fBccomp\fR, is a native-code compiler for a
nearly-complete subset of C99 and a strict superset of MISRA-C 2004. It
produces code with performance characteristics comparable to that generated by
\fBgcc(1)\fR at the \fB\-O1\fR optimization level.
CompCert is unique among compilers in that it is written inside the Coq proof
assistant, and its correctness has been formally verified. That is, the Coq
developers have mathematically proven that (modulo some minor assumptions) a
program compiled with \fBccomp\fR will behave exactly as specified by the
semantics of the original C source.
.SH "RECOGNIZED SOURCE FORMATS"
\fBccomp\fR recognizes source files with the following extensions.
.TP
\fB.c\fR
C source code that must be preprocessed
.TP
\fB.i\fR, \fB.p\fR
C source code that should not be preprocessed
.TP
\fB.cm\fR
Cminor source code
.TP
\fB.s\fR
assembler code
.TP
\fB.S\fR
assembler code that must be preprocessed
.TP
\fB.o\fR
object code
.TP
\fB.a\fR
library archive
.SH OPTIONS
The following options modify \fBccomp\fR's behaviour.
.SS "General options"
.TP
\fB\-stdlib\fR \fIdir\fR
Set the path to CompCert's runtime library.
.TP
\fB\-v\fR
Print each external command before invoking it.
.TP
\fB\-timings\fR
Show the time spent in various compiler passes.
.SS "Processing options"
.TP
\fB\-E\fR
Stop execution after preprocessing and emit preprocessed code on standard output.
.TP
\fB\-S\fR
Compile, but do not link; save generated assembly as a .s file.
.TP
\fB\-c\fR
Compile, but do not link; save generated object code as a .o file.
.TP
\fB\-o\fR \fIfile\fR
Save output as \fIfile\fR.
.SS "Preprocessing options"
.TP
\fB\-I\fR\fIdir\fR
Add \fIdir\fR to the preprocessor search path.
.TP
\fB\-D\fR\fIsymb\fR=\fIval\fR
Define a preprocessor symbol.
.TP
\fB\-U\fR\fIsymb\fR
Undefine a preprocessor symbol.
.TP
\fB\-Wp\fR,\fIopt\fR
Pass option \fIopt\fR to the preprocessor.
.SS "Language support options"
Each of these options may be disabled by specifying \fB\-fno-\fIopt\fR. For
instance, specifying \fB\-fbitfields\fR forces struct bit field emulation;
specifying \fB\-fno-bitfields\fR explicitly disables such emulation.
.TP
\fB\-fbitfields\fR
Emulate bit fields in structs. Disabled by default.
.TP
\fB\-flongdouble\fR
Treat \fBlong double\fR as \fBdouble\fR. Disabled by default.
.TP
\fB\-fstruct-return\fR
Emulate returning structs and unions by value. Disabled by default.
.TP
\fB\-fvararg-calls\fR
Support calls to variable-argument functions. Enabled by default.
.TP
\fB\-funprototyped\fR
Support calls to old-style functions without prototypes. Enabled by default.
.TP
\fB\-fpacked-structs\fR
Emulate packed structs. Disabled by default.
.TP
\fB\-finline-asm\fR
Support inline assembly. Disabled by default.
.TP
\fB\-fall\fR
Enable all language support options.
.TP
\fB\-fnone\fR
Disable all language support options.
.SS "Debugging options"
.TP
\fB\-g\fR
Place debugging information in generated code.
.SS "Code generation options"
Each binary option of the form \fB\-f\fIopt\fR may be disabled by specifying
\fB\-fno-\fIopt\fR. For instance, specifying \fB\-ftailcalls\fR enables
tail-call optimization; \fB\-fno-tailcalls\fR explicitly disables such
optimization.
.TP
\fB\-O\fR
Optimize for speed. This is the default.
.TP
\fB\-Os\fR
Optimize for size.
.TP
\fB\-ffpu\fR
Use floating-point registers for some integer operations. Enabled by default.
.TP
\fB\-fsmall-data\fR \fIn\fR
Set maximal size for allocation in the small data area to be \fIn\fR.
.TP
\fB\-fsmall-const\fR \fIn\fR
Set maximal size for allocation in the small constant area to be \fIn\fR.
.TP
\fB\-ffloat-const-prop\fR \fIn\fR
Control constant propagation of floating-point values. With \fIn\fR set to 0,
disable all float constant propagation; with \fIn\fR set to 2, enable all float
constant propagation. Setting \fIn\fR to 1 enables limited but not total
constant propagation. Default is 2.
.TP
\fB\-ftailcalls\fR
Optimize function calls in tail position. Enabled by default.
.TP
\fB\-falign-functions\fR \fIn\fR
Ensure that function entry points are aligned to multiples of \fIn\fR bytes.
.TP
\fB\-falign-branch-targets\fR \fIn\fR
Ensure that every branch target is aligned to a multiple of \fIn\fR bytes.
.TP
\fB\-falign-cond-branches\fR \fIn\fR
Ensure that every conditional branch is aligned to a multiple of \fIn\fR bytes.
.SS "Target processor options"
.TP
\fB\-mthumb\fR
(ARM only) Use Thumb-2 instruction encoding.
.TP
\fB\-marm\fR
(ARM only) Use ARM instruction encoding.
.SS "Assembling options"
.TP
\fB\-Wa\fR,\fIopt\fR
Pass option \fIopt\fR to the assembler.
.SS "Linking options"
.TP
\fB\-l\fR\fIlib\fR
Link against library \fIlib\fR.
.TP
\fB\-L\fR\fIdir\fR
Add directory \fIdir\fR to the search path for libraries.
.TP
\fB\-Wl\fR,\fIopt\fR
Pass option \fIopt\fR to the linker.
.SS "Tracing options"
.TP
\fB\-dparse\fR
Save C file after parsing and elaboration as \fIfile\fR.parse.c.
.TP
\fB\-dc\fR
Save generated CompCert C as \fIfile\fR.compcert.c.
.TP
\fB\-dclight\fR
Save generated Clight as \fIfile\fR.light.c.
.TP
\fB\-dcminor\fR
Save generated Cminor as \fIfile\fR.cm.
.TP
\fB\-drtl\fR
Save RTL at various optimization points as \fIfile\fR.rtl.\fIn\fR.
.TP
\fB\-dltl\fR
Save LTL after register allocation as \fIfile\fR.ltl.
.TP
\fB\-dmach\fR
Save generated Mach code as \fIfile\fR.mach.
.TP
\fB\-dasm\fR
Save generated assembly as \fIfile\fR.s.
.TP
\fB\-sdump\fR
Save information for post-linking validation as \fIfile\fR.sdump.
.SS "Interpreter mode"
.TP
\fB\-interp\fR
Execute the given C file using the reference interpreter.
.TP
\fB\-quiet\fR
Suppress diagnostic messages from the interpreter.
.TP
\fB\-trace\fR
Have the interpreter produce a detailed trace of reductions.
.TP
\fB\-random\fR
Randomize execution order.
.TP
\fB\-all\fR
Simulate all possible execution orders.
.SH "SEE ALSO"
\&\fIcoqc\fR\|(1), \fIgcc\fR\|(1)
.SH AUTHOR
CompCert is the work of many authors at the Institut National de Recherche en
Informatique et en Automatique (INRIA). Benjamin Barenblat wrote this manual
page.
.SH COPYRIGHT
CompCert is copyright \(co 2004-2014 Institut National de Recherche en
Informatique et en Automatique. It is \fInot\fR free software: you can use it
for evaluation, research, and education purposes, but not for commercial
purposes. See the INRIA Non-Commercial License Agreement
<http://compcert.inria.fr/doc/LICENSE> for further details.
This manual page is copyright \(co 2014, 2015 Benjamin Barenblat and licensed
under the GNU GPL version 3 or later.
|
