CompCert release 18.10

New features

  • New versions of the isel/usel builtin functions for signed and unsigned long long as well as _Bool.
  • CompCert now defines the C11 type max_align_t, a type whose alignment requirement is at least as strict (large) as that of every scalar type.
  • Extended configuration editor to allow specification of additional preprocessor options.
  • String literals are now accepted as l-values and their address can be taken.
  • CompCert now rejects invalid unnamed parameters in function definitions.

Improved handling of _Alignof and _Alignas

  • _Alignof now only accepts types as arguments and returns the natural alignment in bytes.
  • _Alignas is now rejected in illegal places such as typedefs, bit-fields, functions and register class variables.
  • More GCC-compatible handling of the aligned attribute, analogously to the _Alignas operator.
  • CompCert now allows _Alignas(0) intending no alignment change.

Diagnostics

  • New diagnostics for:
    • tentative static definitions with incomplete types
    • unknown attributes used for function parameters
    • alignment requests that reduce the alignment below the natural alignment
    • external function declarations after definitions
    • definitions and uses of static variables in nonstatic inline functions
    • nested structs with flexible array members and structures containing only flexible array members
    • illegal uses of _Alignas as outlined above
  • Diagnostics for C11 extensions are now disabled by default. They can be re-enabled by specifying “-Wc11-extensions”.
  • Improved diagnostics for type-qualified arrays.
  • Improved the wording and unified the formatting of various diagnostics messages.

Valex

New configurable check for correct placement of symbols in sections.

Other improvements

  • Local re-definitions of typedefs are now allowed.
  • CompCert now rejects non-standard applications of the restrict type qualifier.
  • Improved support for type-qualified arrays.
  • Improved support for long long in extended assembler statements for the hybrid PowerPC backend.
  • CompCert now inserts NOP instructions after AIS annotations when the annotation is followed by a label.

Fixes

  • CompCert no longer accepts the comma operator in constant expressions.
  • Fix for abortion in assembling pass caused by overly large branch distances on 64-bit PowerPC platforms. The overflow could be triggered by the use of large 64-bit integer immediate constants in the code between the branch and its branch target.
  • Fixed the passing of the option -u to the linker to mark a symbol as undefined.