CompCert release 15.10

DWARF support

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

Valex

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

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 Synchronize
__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

Fixes

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

Usability

  • 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 gene­rated assembler files and into the DWARF debugging information.

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

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