CompCert Release 15.10

DWARF support
DWARF2 debugging information is now written for the Diab and GCC backends.

New language features
* Added an implicit "return 0" for main() without return.
* Set and clear the CR6 bit before calling an unprototyped
  function to support unprototyped variable argument functions.
* Fixed issue with parsing of type names which occur
  if a typedef name is used after a for loop that uses
  the same name for a loop variable.
* Allow redefinitions of typedefs with the same name and same type
  as specified in ISO/IEC 9899:201x 6.7p3 bullet point 1.
* Added support for bitfield members in unions.

New built-in functions
Note: the built-ins are for a PPC architecture in embedded mode only.

- __builtin_set_spr(spr,val)
  Moves "val" to special purpose register "spr"

- result = __builtin_get_spr(spr)
  Returns the value of the special purpose register "spr" in "result"

- __builtin_prefetch(ea,rw=0/1,ct=0/1/2)
  Data Cache Block (rw=0) or
  Data Cache Block for Store (rw=1)

- __builtin_dcbf(ea)
  Data Cache Block Flush

- __builtin_dcbt(ea)
  Data Cache Block Touch

- __builtin_dcbtls(ea,ct=0/2)
  Data Cache Block Touch and Lock Set

- __builtin_dcbi(ea)
  Data Cache Block Invalidate

- __builtin_dcbz(ea)
  Data Cache Block set to Zero

- __builtin_icbtls(ea,ct=0/2)
  Instruction Cache Block Touch and Lock Set

- __builtin_icbi(ea)
  Instruction Cache Block Invalidate

- __builtin_mbar(mo=0/1)
  Memory Barrier

- __builtin_isync()
  Instruction Synchronize

- __builtin_sync() / __builtin_lwsync

- __builtin_cmpb(result,a,b)
  Compare Bytes

- __atomic_exchange(ea0,ea1,result)
  Atomic Exchange:
  stores the contents of "*ea1" into "*ea0"
  while the original value of "*ea0" is copied to "*result"

- result = __atomic_compare_exchange(ea,expected,desired)

  Atomic Compare and Exchange:
  compares the content of "*ea" to that of "*expected";
  if these are equal, the operation is a read-modify-write
  that writes "*desired" into "*ea" and the returned value
  "result" is "1"; if they are not equal, the operation is
  a read and the current content of "*ea" is written into
  "*expected" while the returned value "result" is "0"

- __atomic_load(source,destination)
  Atomic Load:
  returns the contents of "*source" in "*destination"

- result = __sync_fetch_and_add(ea,val)
  Syncronize Fetch and Add:
  increments the content of "*ea" by "val" and returns
  the previous value of "*ea"

- result = __builtin_clz(val)
  Count Leading Zeros in "val"

- result = __builtin_isel(e, vala, valb)
  Returns "vala" if the given boolean expression "e" is true,
  and "valb" otherwise

* Added the Valex tool for postpass validation of the executable
  assembled/linked with the WindRiver Diab or GCC toolchain.
* New serialization of the assembler AST in ".json" format.
* Static functions are renamed to avoid name clashes;
  "<f>" becomes "_<file>_<f>".

* Faster parsing of floating point numbers with large exponents.
* Subtraction of two pointers produces now a signed result.
* When assigning to a bit field of type "_Bool",
  the right-hand side is now normalized to "0" or "1"
  via a cast to "_Bool".
* Fixed the printing of assembly output of the "stwux"
  and "cntlzw" instructions.
* Reject non-void functions with incomplete return types.
* Reject more cases of unstructured control flow in switch statements.
* Resolved issue with struct return to an overlapping struct.
* The implict type of the wchar_t type and the typedef
  in the stddef header are now compatible to the WindRiver
  Diab C compiler.
* More conservative pointer analysis to avoid optimizations
  on code that casts pointer to integer and back.

* CompCert standard headers no longer lead to incompatible
  type definitions.
* Added support for anonymous structs and unions in the debug type
  information as well as forward declarations of structs and unions.
* CompCert now writes its build number along with a version string
  and compile-time options to the generated assembler files and into
  the Dwarf debugging information.

Known issues
If any of the following features are used, code correctness cannot
be guaranteed in the current version of CompCert and must be checked

* External variable declarations in block scope are not supported.
* The result of casts between pointer and integer types with sizes
  other than 32 bit are undefined in the CompCert C semantics.
* The bitfield layout of CompCert is incompatible with the bitfield
  layout of the WindRiver Diab C compiler.
* Function parameters of type "float" that are passed
  via the stack are passed as 4-byte single precision values.
  This behaviour differs from that of the Windriver Diab C compiler,
  which converts float arguments to double precision when passing
  them via the stack.
* Types introduced in sizeof and cast expressions cannot be used
  after said expressions. The scopes are not correct.
* CompCert may fail to parse empty initializer lists for array variables.
* Wide string literals are parsed incorrectly when they contain
  non-ASCII wide characters.
* Compcert currently cannot compile K&R functions with incompatible
  prototype definitions.
* CompCert may fail to parse (partial) initialization of multi-dimensional
  arrays if braces are missing.
* Compiling several C files with debug information at once may fail.

Last modified on 9 October 2015 by
Copyright 2015 AbsInt.
An HTML version of these release notes is available at