CompCert release 19.04
New features
- New command-line option
-f(no-)common
that controls the placement of global variables defined without an initializer,
known as tentative definitions in the C standard.
- New diagnostic for usage of reserved keywords
_Imaginary
and _Complex
.
Improvements
- Revised handling of attributes such that they behave more like in GCC and Clang.
CompCert now distinguishes between attributes that attach to names
(variables, fields, typedefs, structs and unions) and those that attach
to objects (variables). In particular, the
aligned(N)
attribute now attaches to names, while the _Alignas(N)
modifier
still attaches to objects.
- Improved overflow detection for integer literals.
The previous check was incomplete for integer literals in base 10.
Fixes
- Improved scoping in declaration lists that involve newly introduced variables.
- Improved scoping of iteration and selection statements. A new scope is now opened for each of them.
- Improved definition of the
NULL
macro to avoid problems
when used as argument to variadic functions on 64-bit platforms.
- The macro
__bool_true_false_are_defined
was missing from <stdbool.h>
.
- Relaxed constraints on debug range generation.
- Now avoiding the generation of several empty range expressions in debug information.
- No debugging information is now generated for non-static inline functions
and functions that are optimized out.
- DWARF range entries are now more compliant with the DWARF 3 standard.