Chapter 3 Using the CompCert C compiler

This chapter explains how to invoke the CompCert C compiler and describes its command-line interface.

3.1 Overview

The CompCert C compiler is a command-line executable named ccomp. Its interface similar to that of many other C compilers. An invocation of ccomp is of the form

By default, every input file is processed in sequence to obtain a compiled object file; then, all compiled object files thus obtained, plus those given on the command line, are linked together to produce an executable program. The name of the generated executable is controlled with the -o option; it is a.out if no option is given. The -c, -S and -E options allow the user to stop this process at an intermediate stage. For example, the -c option stops compilation before invoking the linker, leaving the compiled object files (with extension .o) as the final result. Likewise, the -S option stops compilation before invoking the assembler, leaving assembly files with the .s extension as the final result.

CompCert C accepts several kinds of input files:

.c  C source files

Arguments ending in .c are taken to be source files written in C. Given the file x.c, the compiler preprocesses the file, then compiles it to assembly language, then invokes the assembler to produce an object file named x.o.

.i or .p  C source files that should not be preprocessed

Arguments ending in .i or .p are taken to be source files written in C and already preprocessed, or not using any preprocessing directive. These files are not run through the preprocessor. Given the file x.i or x.p, the compiler compiles it to assembly language, then invokes the assembler to produce an object file named x.o.

Note: CompCert assumes for such files that all occurrences of character sequences where a backslash is immediately followed by a newline character are already removed. Such character sequences can interfere with the correct recognition of comments.

This is normally ensured by the preprocessor, as translation phases 1 and 2.

.s  Assembly source files

Arguments ending in .s are taken to be source files written in assembly language. Given the file x.s, the compiler passes it to the assembler, producing an object file named x.o.

.S  Assembly source files that must be preprocessed

Arguments ending in .S are taken to be source files written in assembly language plus C-style macros and preprocessing directives. Given the file x.S, the compiler passes the file through the C preprocessor, then through the assembler, producing an object file named x.o.

.o  Compiled object files

Arguments ending in .o are taken to be object files obtained by a prior run of compilation. They are passed directly to the linker.

.a  Compiled library files

Arguments ending in .a are taken to be libraries. Like .o files, they are passed directly to the linker.

-llib  Compiled library files

Arguments starting in -l are taken to be system libraries. They are passed directly to the linker.

Here are some examples of use. To compile the single-file program src.c and create an executable called exec, just do

   ccomp -o exec src.c

To compile a two-file program src1.c and src2.c, do

   ccomp -c src1.c
   ccomp -c src2.c
   ccomp -o exec src1.o src2.o

To see the generated assembly code for src1.c, do

   ccomp -S src1.c

3.1.1 Response files

CompCert can read command line arguments from response files passed via @filename, too. The options read from a response file replace the @filename option. If a response file does not exist or cannot be read, the option will be treated literally and is not removed.

Within a response file, the options are separated by whitespace, i.e. by space, tab, or newline characters. Options can be enclosed in either single or double quotes to allow whitespace as part of an option. Furthermore, any character can be escaped by prefixing it with a backslash character.

Including options via response files works recursively, i.e. it is possible to specify @otherfile from within a response file. Circular includes are detected and treated as error.

3.1.2 Configuration files

CompCert reads its target configuration from a file that can be specified in different ways. The following list describes the search order for configuration files with decreasing precedence:

Commandline option  -conf <file>

If specified, CompCert reads its configuration from <file>.

Environment variable  COMPCERT_CONFIG

If present, the environment variable denotes the path to the configuration file to be used.

Commandline option  -target target-triple

If specified, CompCert reads its target configuration from a file named <target-triple>.ini. CompCert searches the configuration file in the bin/, share/, or share/compcert/ subfolders of its installation directory.

Default configuration  compcert.ini

As fallback CompCert looks for a default configuration file named compcert.ini in the same folders as described for the -target option. Such a default configuration is created when CompCert is built from sources.

3.2 Options

The ccomp command recognizes the following options. All options start with a minus sign (-).

3.2.1 Options controlling the output

-c

Compile or assemble the source files, but do not link. The final output is an object file x.o for every input file x.c or x.s or x.S. The name of the output can be controlled using the -o option.

-S

Compile the source files all the way to assembly, but do not assemble nor link. The final output is an assembly file x.s for every input file x.c. The name of the output can be controlled using the -o option.

-E

Stop after the preprocessing stage; do not compile nor link. The output is preprocessed C source code for every input file x.c. If no -o option is given, the preprocessed code is sent to the standard output. If a -o option is given, the preprocessed code is saved to the indicated file.

-o file

Generate the final output in file named file. If none of the -c, -S or -E options are given, the final output is the executable program produced during the linking phase. The -o file option causes this executable to be placed in file. Otherwise, it is placed in file a.out in the current directory.

If the -c option is given along with the -o option, the object file generated by the compilation of the source file given on the command line is saved in file. If no -o option is given, it is generated in the current directory with extension .o.

If the -S option is given along with the -o option, the assembly file generated by the compilation of the source file given on the command line is saved in file. If no -o option is given, it is generated in the current directory with extension .s.

If the -E option is given along with the -o option, the result of preprocessing the source file given on the command line is saved in file. If no -o option is given, the preprocessed result is sent to standard output.

When the -o option is given in conjunction with one of the -c, -S or -E options, there must be only one source file given on the command line.

-sdump

In addition to the outputs normally produced by Compcert, generate a x.sdump file for every x.c input file. The .sdump file contains the abstract syntax tree for the generated assembly code, in JSON format. The .sdump files can be used by the Valex validation tool distributed by AbsInt.

3.2.2 Preprocessing options

-Idir

Add directory dir to the list of directories searched for included .h files.

-Dname

Define name as a macro that expands to “1”. This is equivalent to adding a line “#define name 1” at the beginning of the source file.

-Dname=def

Define name as a macro that expands to def. This is equivalent to adding a line “#define name def” at the beginning of the source file. A parenthesized list of parameters can occur between name and the = sign, to define a macro with parameters. For example, -DF(x,y)=x is equivalent to adding a line “#define F(x,y) x” at the beginning of the source file.

-Uname

Erase any previous definition of the macro name, either built-in or performed via a previous -D option. This is equivalent to adding a line “#undef name” at the beginning of the source file.

-Wp,opt

Pass opt as an option to the preprocessor. If opt contains commas (,), it is split into multiple options at the commas.

-Xpreprocessor opt

Pass opt as an option to the preprocessor.

The macro __COMPCERT__ is always predefined, with expansion “1”.

The macros __COMPCERT_MAJOR__, __COMPCERT_MINOR__ and __COMPCERT_VERSION__ are awlays predefined, with expansions the major version number of CompCert, the minor version number, and a combined version number. For instance, CompCert version 3.7 predefines __COMPCERT_MAJOR__ to 3, __COMPCERT_MINOR__ to 7, and __COMPCERT_VERSION__ to 307.

Refer to section 5 (§6.10.8 Predefined macro names) for further standard predefined macros used by CompCert.

The preprocessing options above can either be concatenated with their arguments (as shown above) or separated from their arguments by spaces.

For GNU backends the options -C, -CC, -finput-charset, -idirafter, -imacros, -iquote, -isystem, -M, -MF, -MG, -MM, -MP, -MQ, -MT, -nostdinc, and -P are recognized and propagated to the preprocessor.

3.2.3 Optimization options

-O        (default mode)

Optimize the code with the objective of improving execution speed. This is the default.

-O1 / -O2 / -O3

Synonymous for -O (optimize for speed).

-Os

Optimize the code with the objective of reducing the size of the executable. CompCert’s optimizations improve both execution speed and code size, but some of the code generation heuristics in -O mode favor speed over compactness. The -Os option biases these heuristics in the other direction, favoring compactness over speed.

-Obranchless

Optimize to generate fewer conditional branches and use branch-free instruction sequences instead. When -fif-conversion is enabled, the conversion is peformed aggressively even if the resulting code is less performant.

-O0

Turn most optimizations off. This produces slower code but reduces compilation times. Equivalent to -fno-const-prop -fno-cse -fno-if-conversion -fno-inline -fno-redundancy -fno-tailcalls. The only optimizations performed are 1- integer constant propagation within expressions, 2- register allocation, and 3- dead code elimination.

-fconst-prop / -fno-const-prop

Turn on/off the constant propagation optimization. Enabled by default.

-fcse / -fno-cse

Turn on/off the elimination of common subexpressions. Enabled by default.

-fif-conversion / -fno-if-conversion

Turn on/off generation of conditional moves for simple if-then-else statements or the conditional operator (?:). If-conversion is heuristics based and selects only small and balanced expressions for optimization. The target architecture must also provide a conditional move instruction suitable for the type of the expression. Enabled by default.

-finline / -fno-inline

Turn on/off the inlining of functions. Enabled by default.

-finline-functions-called-once / -fno-inline-functions-called-once

Turn on/off inlining of functions only required by a single caller. Enabled by default.

-fredundancy / -fno-redundancy

Turn on/off the elimination of redundant computations and useless memory stores. Enabled by default.

-ftailcalls / -fno-tailcalls

Turn on/off the optimization of function calls in tail position. Enabled by default.

-ffloat-const-prop N

This option controls whether and how floating-point constants are propagated at compile-time. The constant propagation optimization consists in evaluating, at compile-time, arithmetic and logical operations whose arguments are constants, and replace these operations by the constants just obtained. A constant, here, is either an integer or float literal, the initial value of a const variable, or, recursively, the result of an arithmetic or logical operation itself contracted by constant propagation. The -ffloat-const-prop controls how floating-point constants are propagated and translated.

-ffloat-const-prop 2        (default mode)

Full propagation of floating-point constants. Float arithmetic is performed by the compiler in IEEE double precision format, with round-to-nearest mode. This propagation is correct only if the program does not change float rounding mode at run-time, leaving it in the default round-to-nearest mode.

-ffloat-const-prop 0

No propagation of floating-point constants. This option should be given if the program changes the float rounding mode during its execution.

-ffloat-const-prop 1

Propagate floating-point constants, assuming round-to-nearest mode, but only for arguments of integer-valued operations such as float comparisons and float-to-integer conversions. In other words, floating-point constants are propagated, but no new floating-point constants are inserted in the generated assembly code. This option is useful for some processor configurations where floating-point constants are stored in slow memory and therefore loading a floating-point constant from memory can be slower than recomputing it at run-time.

3.2.4 Code generation options

-falign-functions N

Force the entry point to any compiled function to be aligned on an N byte boundary. The default alignment for function entry points is 16 bytes for the IA32 target and 4 bytes for the ARM and PowerPC targets.

-falign-branch-targets N

This option is specific to the PowerPC target. In the generated assembly code, align the targets of branch instructions to a multiple of N bytes. Only branch targets that cannot be reached by fall-through execution are thus aligned. If no -falign-branch-targets option is specified, alignment handling for branch targets is deactivated.

-falign-cond-branches N

This option is specific to the PowerPC target. It causes conditional branch instructions (bc) to be aligned to a multiple of N bytes in the generated assembly code. If no -falign-cond-branches option is specified, alignment handling for conditional branch instructions is deactivated.

-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. By default the use of the common section is enabled.

-fno-fpu

Prevent the generation of floating-point or SSE2 instructions for assignments between composites (structures or unions) and for the __builtin_memcpy_aligned built-in function.

-fsmall-data N

This option is specific to the PowerPC EABI target platform with Diab tools. It causes global variables of size less than or equal to N bytes and of non-const type to be placed in the small data area (SDA) of the generated executable, and to be addressed by 16-bit offsets relative to the SDA register. This is more efficient than the default absolute addressing used to access global variables. If no -fsmall-data option is given, N is taken to be 8 by default.

It is possible to use the -fsmall-data option with GNU based PowerPC backends, provided that SDA section and register are correctly set up. However, the option currently can cause problems with static uninitialized variables that are still placed in the .bss section and will result in assembler errors. It is recommended to use the -fno-common option to avoid this.

-fsmall-const N

Similar to -fsmall-data N, but governs the placement of const global variables in the small data area. Remarks for GNU based backends apply analogously.

-Wa,opt

Pass opt as an option to the assembler. If opt contains commas (,), it is split into multiple options at the commas.

-Xassembler opt

Pass opt as an option to the assembler.

3.2.5 Target processor options

-target target-triple

Select a specific target processor configuration for code generation instead of using the default described in compcert.ini. Refer to section 3.1.2 for detailed information about configuration files.

-mthumb

This option applies only to the ARM port of CompCert. It instructs CompCert to generate code using the Thumb2 instruction encoding. This is the default if CompCert was configured for the ARMv7M profile.

-marm

This option applies only to the ARM port of CompCert. It instructs CompCert to generate code using the classic ARM instruction encoding. This is the default if CompCert was configured for a profile other than ARMv7M.

3.2.6 Target toolchain options

-t tof:env

This option is specific to the PowerPC EABI target platform with Diab toolchain. It selects the target architecture and execution environment and is forwarded to the preprocessor, assembler and linker of the Diab toolchain. It has no effect on the code generated by CompCert.

3.2.7 Debugging options

-g

Generate full debugging information in DWARF format. Programs compiled and linked with the -g option can be debugged using a debugger such as GDB.

-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.

-gdwarf-2 / -gdwarf-3

Available for GNU backends to select between debug information in DWARF format version 2 or 3. The default format is DWARF v3.

3.2.8 Linking options

-lx

Link with the system library -lx. The linker searches a standard list of directories for the file libx.a and links it.

-Ldir

Add directory dir to the list of directories searched for -llib libraries.

-Wl,opt

Pass opt as an option to the linker. If opt contains commas (,), it is split into multiple options at the commas.

-WUl,opt

Pass opt as an option to the driver program used for linking. If opt contains commas (,), it is split into multiple options at the commas.

-Xlinker opt

Pass opt as an option to the linker.

For GNU backends the options -nodefaultlibs, -nostartfiles, and -nostdlib are recognized and propagated to the linker.

3.2.9 Language support options

The formally-verified part of the CompCert compiler lacks several features of the C language. Some of these features can be simulated by prior source-to-source transformations, performed during the elaboration phase, before entering the formally-verified part of the compiler. The following language support options control which features are simulated this way. Note that these source-to-source transformations are not formally verified yet and cannot be absolutely trusted. For high-assurance software, it is recommended to deactivate them entirely (option -fnone) or to review the C source code after these transformations (option -dc).

-std=standard

Select the ISO C language standard used. Possible values are c99, c11, and c18. For GNU toolchains the option is passed down to the preprocessor. Specifying the option also enables (c99) or disables (c11, c18) the named warnings of class c11-extensions (see section 3.2.10).

For compatibility with previous CompCert releases, the default, if no -std option is given, is to pass -std=c99 to the preprocessor and disable warning class c11-extensions.

-flongdouble

Accept the long double type and treat it as synonymous for the double type, that is, double-precision IEEE 754 floats. This implementation of long double is correct according to the C standards, but does not conform to the ABIs of the target platforms. In other terms, the code generated by CompCert in -flongdouble mode may not interoperate with code generated by an ABI-conformant compiler.

-fno-longdouble (default)

Reject all occurrences of the long double type.

-fpacked-structs

Enable the programmer to control the alignment of struct types and of their individual fields, via the non-standard packed type attribute (section 6.2).

-fno-packed-structs (default)

Ignore the packed type attribute, and always use the field alignment rules specified by the ABI of the target platform.

-fstruct-passing

Support functions that take parameters and return results of composite types (struct or union types) by value.

-fno-struct-passing (default)

Reject all functions that take arguments or return results of struct or union types.

-funprototyped (default)

Support the declaration and invocation of functions declared without function prototypes (“old-style” unprototyped functions).

-fno-unprototyped

Reject all functions that are not declared with a function prototype.

-funstructured-switch

Enable full support for unstructured switch statements via additional source-to-source transformation.

-fno-unstructured-switch (default)

Reject unstructured forms of switch statements.

-fvararg-calls (default)

Support defining functions with a variable number of arguments, and calling such functions. A typical example is the printf function and its variants from the C standard library.

-fno-vararg-calls

Reject all attempts to define or invoke a variable-argument function.

-finline-asm

Activate support for inline assembly statements (see section 6.6). Indiscriminate use of this statement can ruin all the semantic preservation guarantees of CompCert.

-fno-inline-asm (default)

Reject all uses of asm statements.

-fall

Activate all language support options above.

-fnone

Turn off all language support options above.

As listed in the description above, the -fvararg-calls and -funprototyped language support options are turned on by default, and all other are turned off by default.

3.2.10 Diagnostic options

CompCert supports a scheme of named warnings that allows you to individually enable or disable warnings or to treat them as errors. The diagnostic options are:

-Wall

Enable all warnings.

-Wwarning

Enable the specific warning warning. See below for a list of possible warning names.

-Wno-warning

Disable the specific warning warning. See below for a list of possible warning names.

-w

Suppress all warnings.

-Werror

Treat all warnings of CompCert as errors.

-Werror=warning

Treat the specific warning warning as an error. See below for a list of possible warning names.

-Wno-error=warning

Prevent the specific warning warning from being treated as error even if -Werror is specified. See below for a list of possible warning names.

-Wfatal-errors

Treat all errors of CompCert as fatal errors, so that the compilation is aborted immediately.

-fmax-errors=N

Limits the maximum number of error messages to N, at which point CompCert stops processing the source-code. If N is 0 (default) the number of error messages is unlimited.

-fdiagnostics-format=format

Set format for location information in diagnostic messages. Possible formats are ccomp (default), msvc or vi.

-fdiagnostics-color

CompCert will print all diagnostic messages with color codes. Colorized output is enabled by default when CompCert is invoked with a TTY output device.

-fno-diagnostics-color

CompCert will print all diagnostic messages as standard ASCII text without colorization. This behavior is the default when CompCert is invoked with a non-TTY as output device.

-fdiagnostics-show-option (default)

Print option name with mappable diagnostics.

-fno-diagnostics-show-option (default)

Disable printing option name with mappable diagnostics.

Warning names  CompCert currently supports the following warning names. The names must be inserted instead of the <warning> placeholder in the diagnostic options described above. E.g. use the option -Werror=c11-extensions to turn warnings related to C11 specific features into errors.

c11-extensions (disabled by default)

Feature specific to C11.

compare-distinct-pointer-types (enabled by default)

Comparison of different pointer types.

compcert-conformance (disabled by default)

Features that are not part of the CompCert C core language, e.g. K&R style functions.

constant-conversion (enabled by default)

Dangerous conversion of constants, e.g. literals that are too large for the given type.

extern-after-definition (enabled by default)

Extern declarations after non-extern definitions.

flexible-array-extensions (disable by default)

Use of structs with flexible arrays nexted within structs or arrays.

gnu-empty-struct (enabled by default)

GNU extension for empty structs.

ignored-attributes (enabled by default)

Attribute declarations after definitions.

implicit-function-declaration (enabled by default)

Deprecated implicit function declarations.

implicit-int (enabled by default)

Type of parameter or return type is implicitly assumed to be int.

inline-asm-sdump (enabled by default)

Use of unsupported features in combination with dump of abstract syntax tree (via option -sdump).

int-conversion (enabled by default)

Conversion between pointer and integer.

invalid-noreturn (enabled by default)

Functions declared as noreturn that actually contain a return statement.

invalid-utf8 (enabled by default)

Illegal unicode characters in string or character constants.

literal-range (enabled by default)

Floating point literals with out-of-range magnitudes or values that convert to NaN.

main-return-type (enabled by default)

Wrong return type for main.

missing-declarations (enabled by default)

Declations which do not declare anything.

non-linear-cond-expr (disabled by default)

Conditional expression that may not be optimized to branchless code. Only issued in -Obranchless mode.

pointer-type-mismatch (enabled by default)

Use of incompatible pointer types in conditional expressions.

reduced-alignment (disabled by default)

Alignment specifications below natural alignment.

return-type (enabled by default)

Void-return statement in non-void function.

static-in-inline (enabled by default)

Use of static variables in non-static inline functions.

tentative-incomplete-static (disabled by default)

Static tentative definition with incomplete type.

unknown-attributes (enabled by default)

Use of unsupported or unknown attributes.

unknown-pragmas (disabled by default)

Use of unsupported or unknown pragmas.

unused-ais-parameter (disabled by default)

Unused parameter for embedded program annotations.

unused-variable (disabled by default)

Unused local variables.

varargs (enabled by default)

Promotable vararg arguments.

wrong-ais-parameter (enabled by default)

Use of illegal parameter expressions for embedded program annotations.

zero-length-array (disabled by default)

GNU extension for zero length arrays.

3.2.11 Tracing options

The following options direct the compiler to save the file being compiled into files at various stages of compilation. The three most useful tracing options are:

-dparse

Save the C file after parsing, elaboration, and source-to-source transformations as described in section “Language support options”. If the source file is named x.c, the intermediate form is saved in file x.parsed.c, in C syntax. This intermediate form is useful to review the effect of the unverified source-to-source transformations.

-dc

Save the generated CompCert C code, just before entering the verified part of the compiler. If the source file is named x.c, the intermediate form is saved in file x.compcert.c, in C syntax. This intermediate form is useful in conjunction with the reference interpreter, because it represents the program exactly as it is interpreted.

-dasm

Save the generated assembly code, just before calling the assembler. If the source file is named x.c, the assembly code is saved in file x.s. Unlike with option -S, compilation does not stop here and continues with assembling and linking.

The remaining tracing options are of interest mainly to the CompCert developers. In the description below, we assume that the source file is named x.c.

-dclight

Save generated Clight intermediate code in file x.light.c, in C-like syntax.

-dcminor

Save generated Cminor intermediate code in file x.cm.

-drtl

Save generated RTL form at successive stages of optimization in files x.rtl.0, x.rtl.1, etc.

-dltl

Save LTL form after register allocation in x.ltl

-dmach

Save Mach form after stack layout in file x.mach

3.2.12 Miscellaneous options

-v

Before every invocation of an external command (preprocessor, assembler, linker), print the command and its arguments.

-timings

Measure and display the time spent in various compilation passes.

-stdlib dir

Specify the directory dir containing the CompCert C specific library and header files. This option is useful in the rare case where the user needs to override the default location specified at CompCert installation time.

-conf file

Read CompCert configuration from file. This takes precedence over any other specification. Refer to section 3.1.2 for detailed information about configuration files.