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.