.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 Read CompCert configuration from . This takes precedence over any other specification. . .TP .B \-target Read CompCert configuration from .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 : Select target for Diab toolchain. The option is forwarded to the Diab toolchain and has no effect on the code generated by CompCert. denotes the \fIt\fParget processor, \fIo\fPbject file format and \fIf\fPloating point support. denotes the execution \fIenv\fPironment. . .SS Processing Options .INDENT 0.0 . .TP .B \-c Compile to object file only (no linking), result in .o. . .TP .B \-E Preprocess only, send result to standard output. . .TP .B \-S Compile to assembly only, save result in .s. . .TP .B \-o Generate output to . . .SS Preprocessing Options .INDENT 0.0 . .TP .B \-I Add to search path for include files. . .TP .B \-include Process as if \fB#include ""\fP appears at the first line of the primary source file. . .TP .B \-D= Define a preprocessor symbol. . .TP .B \-U Undefine a preprocessor symbol. . .TP .B \-Wp, Pass comma separated arguments in to the preprocessor. . .TP .B \-Xpreprocessor Pass argument to the preprocessor. . .TP .BR \-C ", " \-CC ", " \-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 Control constant propagation of floats (=0: none, =1: limited, =2: full). Default is full constant propagation. . .SS Code Generation Options .INDENT 0.0 . .TP .B \-falign\-functions Set alignment of function entry points to 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 Set alignment of branch targets to bytes. By default alignment of branch targets is deactivated. . .TP .B \-falign\-cond\-branches Set alignment of conditional branch instructions to bytes. By default alignment of conditional branches is deactivated. . .SS Code Generation Options (PowerPC with Diab Backend) .INDENT 0.0 . .TP .B \-fsmall\-const Set maximal size for allocation in small data constant to bytes. The default is 8 bytes. . .TP .B \-fsmall\-data Set maximal size for allocation in small data area to 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 ARMv7R profile. . .TP .B \-marm Generate code using the ARM instruction encoding. This is the default if CompCert is configured for a profile other than ARMv7R. . .SS Assembling Options .INDENT 0.0 . .TP .B \-Wa, Pass comma separated arguments in to the assembler. . .TP .B \-Xassembler Pass argument 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- 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 Link library . . .TP .B \-L Add to search path for libraries. . .TP .B \-Wl, Pass comma separated arguments in to the linker. . .TP .B \-WUl, Pass comma separated arguments in to the driver program used for linking. . .TP .B \-Xlinker Pass argument 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 Use as linker command file. . .TP .B \-u Pretend the 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 \-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 \-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 Enable the specific 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 unsupported features 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 \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 \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- Disable the specific warning . . .TP .B \-w Suppress all warnings. . .TP .B \-Werror Treat all warnings of CompCert as errors. . .TP .B \-Werror= Treat the specific warning as an error. . .TP .B \-Wno-error= Prevent the specific 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= Print at most error messages before bailing out. Defaults to =0 which means unlimited error messages. . .TP .B \-fdiagnostics\-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 .i . .TP .B \-dparse Save C file after parsing and elaboration in .parsed.c. . .TP .B \-dc Save generated CompCert C in .compcert.c. . .TP .B \-dclight Save generated Clight in .light.c. . .TP .B \-dcminor Save generated Cminor in .cm. . .TP .B \-drtl Save RTL at various optimization points in .rtl.. . .TP .B \-dltl Save LTL after register allocation in .ltl. . .TP .B \-dmach Save generated Mach code in .mach. . .TP .B \-dasm Save generated assembly in .s. . .TP .B \-dall Save all generated intermediate files in .. . .TP .B \-sdump Save abstract syntax tree of generated assembly for post-linking validation tool in .json. . .SS Miscellaneous Options .INDENT 0.0 . .TP .B \-stdlib Set the path of the CompCert run-time library to . . .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 @ Read command line options from . . .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 .