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.


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


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