CompCert release 16.04

DWARF support

DWARF2 debugging information is now written for the IA32 and ARM backends.

New builtins

  • ARM, IA32, and PowerPC:
    • int __builtin_clzl(unsigned long val) and
    • int __builtin_clzll(unsigned long long val)

    Same as __builtin_clz but for long and long long types. Counts leading zeroes in val.

  • PowerPC:
    • unsigned int __builtin_uisel(bool e, unsigned int vala, unsigned int valb)
      Equivalent to __builtin_isel but for unsigned integer types. Returns vala if the given boolean expression e is true, valb otherwise.
    • void __builtin_mr(int dst, int src)
      Moves the contents of the 32-bit general-purpose register src to the 32-bit general-purpose register dst. Note that CompCert does not take the semantics of the regi­ster move into account, i.e. the resulting code may have undefined behavior.
    • void __builtin_set_spr64(int spr, unsigned long long val)
      Moves a 64-bit value val into the 64-bit special-purpose register spr.
    • unsigned long long __builtin_get_spr64(int spr)
      Returns the 64-bit value of the special purpose register spr.

    Note that the 64-bit builtins require 64-bit capable hardware (PowerPC E5500) and also need to be supported by the OS, e.g. with proper state preservation and restoration for interrupts.

New options

  • -gdepth
    for controlling the level of generated debug information
  • -conf
    for specifying the compcert.ini file
  • -target
    for selecting default targets

Other features

  • CompCert now contains a lightweight verification of separate compilation. Semantic preservation is still stated and proved in terms of a whole C program and a whole assembly program. However, the whole C program can be the result of syntactic linking of several C compilation units, each of them being separately compiled by CompCert to produce an assembly unit, and these assembly units then being linked together to produce the whole assembly program.
  • CompCert now recognizes the C11 keyword _Noreturn and produces a warning for any _Noreturn function that contains a return.
  • CompCert now has the C11 stdalign header defining alignas and alignof macros.
  • CompCert now has the standard header iso646.h.

New command line options for GCC compatibility

GCC and Diab frontends:

  • -include <file>
    corresponds to writing #include "<file>" as the first line in the primary source file
  • -s
    removes all symbol table and relocation information from the executable
  • -static
    passes the -static flag to the linker
  • -u <symb>
    pretends the symbol <symb> is undefined to force linking of library modules to define it
  • -Xassembler <opt>
    passes <opt> as an option to the assembler
  • -Xlinker <opt>
    passes <opt> as an option to the linker

GCC frontend only:

  • -C
    Do not discard comments
  • -CC
    Do not discard comments, including during macro expansion
  • -idirafter <dir>
    Search <dir> for header files after all directories specified with -I and the standard system directories
  • -imacros <file>
    Like -include but throws output produced by preprocessing of <file> away
  • -iquote <dir>
    Like -isystem but only for headers included with quotes
  • -isystem <dir>
    Search <dir> for header files after all directories specified by -I but before the standard system directories
  • -M
    Output a rule suitable for make describing the dependencies of the main source file
  • -MM
    Like -M but do not mention system header files
  • -MF <file>
    specifies <file> as the output file for -M or -MM
  • -MG
    Assumes missing header files are generated for -M
  • -MP
    Add a phony target for each dependency other than the main file
  • -MT <target>
    Change the target of the rule emitted by dependency generation
  • -MQ <target>
    Like -MT but quotes <target>
  • -P
    Do not generate linemarkers
  • -nostartfiles
    Do not use the standard system startup files when linking
  • -nodefaultlibs
    Do not use the standard system libraries when linking
  • -nostdinc
    Do not search the standard system directories for header files
  • -nostdlib
    Do not use the standard system startup files or libraries when linking

Other improvements

  • Descriptions of syntax errors are more detailed now, following the pattern “found X but expected Y”.
  • Better error message for Valex in the case of non-matching instructions including arguments for the asm instructions.
  • Added printing functions for debug annotations in C syntax.
  • Valex messages generated during the compare step now include the name of the compilation unit.
  • CompCert passes the -I flags to the assembler.
  • Support for <pointer> +/- <integer> where the pointer value is actually an integer that has been converted to pointer type.

Fixes

  • Compiling several C files with debug information at once now works as expected.
  • A warning introduced by debug statements in switch has been removed.
  • Fixed issue with passing options to the Diab assembler.
  • Debug info is missing for functions when they are declared via a prototype, then defined but never used otherwise in the file.
  • Added the diab data Xalign-value option to enforce interpreting alignment values as values and not powers of two.