CompCert release 20.04

New features

  • New architecture AArch64.
  • Support for vertical tab characters if they are not removed by the preprocessor.

Improved messages

  • New error message for unknown __builtin_ functions.
  • New error messages for malformed section attributes.
  • Improved error message for redefinition of typedefs.

Other improvements

  • Improved printing of types in diagnostic messages.
  • Better treating of inline.
  • Improved handling of location lists in DWARF.
  • The reference interpreter now accepts free(NULL), which according to ISO C is correct and does nothing.
  • The ec_readonly condition is reduced to the strict minimum needed to show the correctness of value analysis for const globals.


  • In strict PowerPC EABI mode, single-precision floating-point arguments passed on stack are passed as a 64-bit word, extended to double precision.
  • Enforced normalization for x86 and AArch64 backends of parts of return values not specified in the ABI.
  • More precise determination of small data accesses to avoid linker errors due to sda offsets that are too large.
  • In PPC Diab, the internal type of wide character constant has been set to wchar_t.
  • In certain rare cases, the int64-to-float32 conversion led to a double rounding. This is now avoided.