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.

Fixes

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