CompCert release 20.04

New features

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


  • New error message for unknown __builtin_ functions.
  • Improved printing of types in diagnostic messages.
  • Improved error message for redefinition of typedefs.
  • 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 too large sda offsets.
  • In PPC Diab, the internal type of wide character constant has been set to wchar_t.