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.

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.


==============================================================================
Last modified on 13 April 2016 by alex@absint.com.
Copyright 2016 AbsInt. www.absint.com
==============================================================================
An HTML version of these release notes is available at
www.absint.com/releasenotes/compcert/16.04