path: root/doc/ccomp.1

.TH CCOMP 1
.SH NAME
ccomp \- the CompCert C compiler
.
.SH SYNOPSIS
\fBccomp\fP [\fIoptions\fP] \fIfile ...\fP
.
.SH DESCRIPTION
\fBCompCert C\fP is a compiler for the C programming language.
Its intended use is the compilation of life-critical and mission-critical software written in C and meeting high levels of assurance.
It accepts most of the ISO C 99 language, with some exceptions and a few extensions.
It produces machine code for the PowerPC (32bit), ARM (32bit), AArch64 (ARM 64bit), x86 (32bit and 64bit), and RISC-V (32bit and 64bit) architectures.
.PP
What sets CompCert C apart from any other production compiler, is that it is formally verified, using machine-assisted mathematical proofs, to be exempt from miscompilation issues.
In other words, the executable code it produces is proved to behave exactly as specified by the semantics of the source C program.
This level of confidence in the correctness of the compilation process is unprecedented and contributes to meeting the highest levels of software assurance.
In particular, using the CompCert C compiler is a natural complement to applying formal verification techniques (static analysis, program proof, model checking) at the source code level: the correctness proof of CompCert C guarantees that all safety properties verified on the source code automatically hold as well for the generated executable.
.
.SH RECOGNIZED SOURCE FILES
.
.TP
.B .c
C source file.
.
.TP
.BR .i ", " .p
C source file that should not be preprocessed.
.
.TP
.B .s
Assembly file.
.
.TP
.B .S
Assembly file that must be preprocessed.
.
.TP
.B .o
Object file.
.
.TP
.B .a
Library file.
.
.SH OPTIONS
.SS General Options
.INDENT 0.0
.
.TP
.B \-conf <file>
Read CompCert configuration from <file>. This takes precedence over any other specification.
.
.TP
.B \-target <triple>
Read CompCert configuration from <triple>.ini instead of using the default of compcert.ini.
The configuration file is searched for in the share directory of the CompCert installation.
.
.SS
Toolchain Options (PowerPC with Diab Backend)
.TP
.B \-t <tof>:<env>
Select target for Diab toolchain. The option is forwarded to the Diab toolchain and has no effect on the code generated by CompCert.
<tof> denotes the \fIt\fParget processor, \fIo\fPbject file format and \fIf\fPloating point support.
<env> denotes the execution \fIenv\fPironment.
.
.SS Processing Options
.INDENT 0.0
.
.TP
.B \-c
Compile to object file only (no linking), result in <file>.o.
.
.TP
.B \-E
Preprocess only, send result to standard output.
.
.TP
.B \-S
Compile to assembly only, save result in <file>.s.
.
.TP
.B \-o <file>
Generate output to <file>.
.
.SS Preprocessing Options
.INDENT 0.0
.
.TP
.B \-I<dir>
Add <dir> to search path for include files.
.
.TP
.B \-include <file>
Process <file> as if \fB#include "<file>"\fP appears at the first line of the primary source file.
.
.TP
.B \-D<symbol>=<value>
Define a preprocessor symbol.
.
.TP
.B \-U<symbol>
Undefine a preprocessor symbol.
.
.TP
.B \-Wp,<args>
Pass comma separated arguments in <args> to the preprocessor.
.
.TP
.B \-Xpreprocessor <arg>
Pass argument <arg> to the preprocessor.
.
.TP
.BR \-C ", " \-CC ", " \-finput-charset ", " \-idirafter ", " \-imacros ", " \-iquote ", " \-isystem ", " \-M ", " \-MF ", " \-MG ", " \-MM ", " \-MP ", " \-MQ ", " \-MT  ", " \-nostdinc ", " \-P
For GNU backends these options are recognized by CompCert and passed through to the preprocessor.
.
.SS
Optimization Options
.INDENT 0.0
.
.TP
.B \-O
Optimize the compiled code.
Enabled by default.
.
.TP
.B \-O0
Turn off most optimizations.
Synonymous to \fB\-fno\-const\-prop\fP \fB\-fno\-cse\fP \fB\-fno\-if\-conversion\fP
\fB\-fno\-inline\fP \fB\-fno\-redundancy\fP \fB\-fno\-tailcalls\fP.
.
.TP
.BR \-O1 ", " \-O2 ", " \-O3
Synonymous for \fB\-O\fP.
.
.TP
.B \-Os
Optimize for code size in preference to code speed.
.
.TP
.B \-Obranchless
Optimize to generate fewer conditional branches and use branch-free
instruction sequences instead.  When \fB-fif\-conversion\fP is
enabled, the conversion is peformed aggressively even if the resulting
code is less performant.
.
.TP
.BR \-fconst\-prop ", " \-fno\-const\-prop
Turn on/off global constant propagation.
Enabled by default.
.
.TP
.BR \-fcse ", " \-fno\-cse
Turn on/off common subexpression elimination.
Enabled by default.
.
.TP
.BR \-fif\-conversion ", " \-fno\-if\-conversion
Turn on/off generation of conditional moves.
Enabled by default.
.
.TP
.BR \-finline ", " \-fno\-inline
Turn on/off inlining of functions.
Enabled by default.
.
.TP
.BR \-finline\-functions\-called\-once ", " \-fno\-inline\-functions\-called\-once
Turn on/off inlining of functions only required by a single caller.
Enabled by default.
.
.TP
.BR \-fredundancy ", " \-fno\-redundancy
Turn on/off redundancy elimination.
Enabled by default.
.
.TP
.BR \-ftailcalls ", " \-fno\-tailcalls
Turn on/off optimization of function calls in tail position.
Enabled by default.
.
.TP
.B \-ffloat\-const\-prop <n>
Control constant propagation of floats (<n>=0: none, <n>=1: limited, <n>=2: full).
Default is full constant propagation.
.
.SS
Code Generation Options
.INDENT 0.0
.
.TP
.B \-falign\-functions <n>
Set alignment of function entry points to <n> bytes.
The default alignment is 16 bytes for x86 targets and 4 bytes for ARM and PowerPC.
.
.TP
.BR \-fcommon ", " \-fno\-common
Turn on/off placement of global variables defined without an initializer (tentative definitions) in the common section.
Disabling the use of the common section inhibits merging of tentative definitions by the linker and may lead to multiple-definition errors.
Enabled by default.
.
.TP
.BR \-ffpu ", " \-fno\-fpu
Turn on/off use of FP registers for some integer operations.
Enabled by default.
.
.SS
Code Generation Options (PowerPC)
.INDENT 0.0
.
.TP
.B \-falign\-branch\-targets <n>
Set alignment of branch targets to <n> bytes.
By default alignment of branch targets is deactivated.
.
.TP
.B \-falign\-cond\-branches <n>
Set alignment of conditional branch instructions to <n> bytes.
By default alignment of conditional branches is deactivated.
.
.SS
Code Generation Options (PowerPC with Diab Backend)
.INDENT 0.0
.
.TP
.B \-fsmall\-const <n>
Set maximal size for allocation in small data constant to <n> bytes.
The default is 8 bytes.
.
.TP
.B \-fsmall\-data <n>
Set maximal size for allocation in small data area to <n> bytes.
The default is 8 bytes.
.
.SS
Code Generation Options (ARM Targets)
.INDENT 0.0
.
.TP
.B \-mthumb
Generate code using the Thumb 2 instruction encoding.
This is the default if CompCert is configured for the ARMv7M profile.
.
.TP
.B \-marm
Generate code using the ARM instruction encoding.
This is the default if CompCert is configured for a profile other than ARMv7M.
.
.SS
Assembling Options
.INDENT 0.0
.
.TP
.B \-Wa,<args>
Pass comma separated arguments in <args> to the assembler.
.
.TP
.B \-Xassembler <arg>
Pass argument <arg> to the assembler.
.
.SS
Debugging Options
.INDENT 0.0
.
.TP
.B \-g
Generate full debugging information.
.
.TP
.BR \-g0 ", " \-g1 ", " \-g2 ", " \-g3
Control generation of debugging information (0: none, 1: only globals, 2: globals and locals without locations, 3: full debug information). The default level is 3 for full debug information.
.
.SS
Debugging Options (GNU Backend)
.INDENT 0.0
.
.TP
.B \-gdwarf-<n>
For GNU backends select debug information in DWARF format version 2 or 3.
The default format is DWARF v3.
.
.SS
Linking Options
.INDENT 0.0
.
.TP
.B \-l<library>
Link library <library>.
.
.TP
.B \-L<dir>
Add <dir> to search path for libraries.
.
.TP
.B \-Wl,<args>
Pass comma separated arguments in <args> to the linker.
.
.TP
.B \-WUl,<args>
Pass comma separated arguments in <args> to the driver program used for linking.
.
.TP
.B \-Xlinker <arg>
Pass argument <arg> to the linker.
.
.TP
.B \-s
Remove all symbol table and relocation information from the executable.
.
.TP
.B \-static
Prevent linking with the shared libraries.
.
.TP
.B \-T <file>
Use <file> as linker command file.
.
.TP
.B \-u <symbol>
Pretend the symbol <symbol> is undefined to force linking of library modules to define it.
.
.TP
.BR \-nodefaultlibs ", " \-nostartfiles ", " \-nostdlib
For GNU backends these options are recognized by CompCert and passed through to the linker.
.
.SS
Language Support Options
.INDENT 0.0
.
.TP
.BR \-std=<standard>
Choose the ISO C language standard to be used: \fBc99\fP, \fBc11\fP, or \fBc18\fP.
Defaults to \fBc99\fP.
.
.TP
.BR \-flongdouble ", " \-fno\-longdouble
Turn on/off support for emulation of \fBlong double\fP as \fBdouble\fP.
Disabled by default.
.
.TP
.BR \-fpacked\-structs ", " \-fno\-packed\-structs
Turn on/off support for emulation of packed structs.
Disabled by default.
.
.TP
.BR \-fstruct\-passing ", " \-fno\-struct\-passing\fR
Turn on/off support for passing structs and unions by value as function results or function arguments.
Disabled by default.
.
.TP
.BR \-funprototyped ", " \-fno\-unprototyped
Turn on/off support calls to old-style functions without prototypes.
Enabled by default.
.
.TP
.BR \-funstructured-switch ", " \-fno\-unstructured-switch
Turn on/off support for non-structured \fBswitch\fP statements.
Disabled by default.
.
.TP
.BR \-fvararg\-calls ", " \-fno\-vararg\-calls
Turn on/off support for calls to variable-argument functions.
Enabled by default.
.
.TP
.BR \-finline-asm ", " \-fno\-inline-asm
Turn on/off support for inline \fBasm\fP statements.
Disabled by default.
.
.TP
.B \-fall
Activate all language support options above.
.
.TP
.B \-fnone
Deactivate all language support options above.
.
.SS
Diagnostic Options
.INDENT 0.0
.
.TP
.B \-Wall
Enable all warnings.
.
.TP
.B \-W<warning>
Enable the specific warning <warning>.
CompCert supports the following warning classes:
.sp
\fIc11\-extensions\fP:
Feature specific to C11.
Disabled by default.
.sp
\fIcompare\-distinct\-pointer\-types\fP:
Comparison of different pointer types.
Enabled by default.
.sp
\fIcompcert\-conformance\fP:
Features that are not part of the CompCert C core language, e.g. K&R style functions.
Disabled by default.
.sp
\fIconstant\-conversion\fP:
Dangerous conversion of constants, e.g. literals that are too large for the given type.
Enabled by default.
.sp
\fIextern\-after\-definition\fP:
Extern declarations after non-extern definitions.
Enabled by default.
.sp
\fIflexible\-array\-extensions\fP:
Use of structs with flexible arrays nexted within structs or arrays.
Disabled by default.
.sp
\fIgnu\-empty\-struct\fP:
GNU extension for empty structs.
Enabled by default.
.sp
\fIignored\-attributes\fP:
Attribute declarations after definitions.
Enabled by default.
.sp
\fIimplicit\-function\-declaration\fP:
Deprecated implicit function declarations.
Enabled by default.
.sp
\fIimplicit\-int\fP:
Type of parameter or return type is implicitly assumed to be int.
Enabled by default.
.sp
\fIinline\-asm\-sdump\fP:
Use of inline assembly in combination with dump of abstract syntax tree.
Enabled by default.
.sp
\fIint\-conversion\fP:
Conversion between pointer and integer.
Enabled by default.
.sp
\fIinvalid\-noreturn\fP:
Functions declared as noreturn that actually contain a return statement.
Enabled by default.
.sp
\fIinvalid\-utf8\fP:
Illegal unicode characters in string or character constants.
Enabled by default.
.sp
\fIliteral\-range\fP:
Floating point literals with out-of-range magnitudes or values that convert to NaN.
Enabled by default.
.sp
\fImain\-return\-type\fP:
Wrong return type for main.
Enabled by default.
.sp
\fImissing\-declarations\fP:
Declarations which do not declare anything.
Enabled by default.
.sp
\fInon\-linear\-cond\-expr\fP:
Conditional expression that may not be optimized to branchless code.
Only issued in \fB-Obranchless\fP mode.
Disabled by default.
.sp
\fIpointer\-type\-mismatch\fP:
Use of incompatible pointer types in conditional expressions.
Enabled by default.
.sp
\fIreduced\-alignment\fP:
Alignment specifications lower than natural alignment.
Disabled by default.
.sp
\fIreturn\-type\fP:
Void-return statement in non-void function.
Enabled by default.
.sp
\fIstatic\-in\-inline\fP:
Use of static variables in non-static inline functions.
Enabled by default.
.sp
\fItentative\-incomplete\-static\fP:
Use of tentative static definitions with incomplete type.
Disabled by default.
.sp
\fIunknown\-attributes\fP:
Use of unsupported or unknown attributes.
Enabled by default.
.sp
\fIunknown\-pragmas\fP:
Use of unsupported or unknown pragmas.
Disabled by default.
.sp
\fIunused\-ais\-parameter\fP:
Unused parameter for embedded program annotations.
Disabled by default.
.sp
\fIunused\-variable\fP:
Unused local variables.
Disabled by default.
.sp
\fIvarargs\fP:
Promotable vararg arguments.
Enabled by default.
.sp
\fIweak\-sdump\fP:
Use of attribute \fBweak\fP in combination with dump of abstract syntax tree.
Enabled by default.
.sp
\fIwrong\-ais\-parameter\fP:
Use of illegal parameter expressions for embedded program annotations.
Enabled by default.
.sp
\fIzero\-length\-array\fP:
GNU extension for zero length arrays.
Disabled by default.
.
.TP
.B \-Wno-<warning>
Disable the specific warning <warning>.
.
.TP
.B \-w
Suppress all warnings.
.
.TP
.B \-Werror
Treat all warnings of CompCert as errors.
.
.TP
.B \-Werror=<warning>
Treat the specific warning <warning> as an error.
.
.TP
.B \-Wno-error=<warning>
Prevent the specific warning <warning> from being treated as error even if \fB\-Werror\fP is specified.
.
.TP
.B \-Wfatal-errors
Treat all errors of CompCert as fatal errors, so that the compilation is aborted immediately.
.
.TP
.B \-fmax\-errors=<n>
Print at most <n> error messages before bailing out.  Defaults to <n>=0 which means unlimited error messages.
.
.TP
.B \-fdiagnostics\-format=<format>
Select format for location information in messages.  Possible formats are \fBccomp\fP (default), \fBmsvc\fP or \fBvi\fP.
.
.TP
.BR \-fdiagnostics\-color ", " \-fno\-diagnostics\-color
Turn on/off colored diagnostics.  Enabled by default for TTY output devices.
.
.TP
.BR \-fdiagnostics\-show-option ", " \-fno\-diagnostics\-show\-option
Turn on/off printing of option name with mappable diagnostics.  Enabled by default.
.
.SS
Tracing Options
.INDENT 0.0
.
.TP
.B \-dprepro
Save C file after preprocessing in <file>.i
.
.TP
.B \-dparse
Save C file after parsing and elaboration in <file>.parsed.c.
.
.TP
.B \-dc
Save generated CompCert C in <file>.compcert.c.
.
.TP
.B \-dclight
Save generated Clight in <file>.light.c.
.
.TP
.B \-dcminor
Save generated Cminor in <file>.cm.
.
.TP
.B \-drtl
Save RTL at various optimization points in <file>.rtl.<n>.
.
.TP
.B \-dltl
Save LTL after register allocation in <file>.ltl.
.
.TP
.B \-dmach
Save generated Mach code in <file>.mach.
.
.TP
.B \-dasm
Save generated assembly in <file>.s.
.
.TP
.B \-dall
Save all generated intermediate files in <file>.<ext>.
.
.TP
.B \-sdump
Save abstract syntax tree of generated assembly for post-linking validation tool in <file>.json.
.
.SS
Miscellaneous Options
.INDENT 0.0
.
.TP
.B \-stdlib <dir>
Set the path of the CompCert run-time library to <dir>.
.
.TP
.B \-v
Print external commands before invoking them.
.
.TP
.B \-timings
Print information about the time spent in various compiler passes.
.
.TP
.B \-version
Print the CompCert version information and exit.
.
.TP
.B @<file>
Read command line options from <file>.
.
.SS
Interpreter Mode
.INDENT 0.0
.
.TP
.B \-interp
Execute the given .c files using the reference interpreter.
.
.TP
.B \-quiet
Suppress diagnostic messages for the interpreter.
.
.TP
.B \-trace
Have the interpreter produce a detailed trace of reductions.
.
.TP
.B \-random
Randomize execution order.
.
.TP
.B \-all
Simulate all possible execution orders.
.
.SH ENVIRONMENT
.
.TP
.B COMPCERT_CONFIG
If this environment variable is present, it denotes the path to the CompCert configuration file to be used.
The variable takes precedence over default search paths or the \fB\-target\fP option, but has a lower priority than the \fB\-conf\fP option.
.
.SH BUGS
.
To report bugs, please visit <https://github.com/AbsInt/CompCert/issues>.