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)
  * 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 register 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>
     dearch <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.

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

Last modified on 13 April 2016 by
Copyright 2016 AbsInt.
An HTML version of these release notes is available at