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.