CompCert Release 20.04 ---------------------- New features ------------------------- ● New architecture AArch64. ● Support for vertical tab characters if they are not removed by the preprocessor. Improvements -------------------------- ● New error message for unknown __builtin_ functions. ● New error messages for malformed section attributes. ● 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. 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 too large sda offsets. ● 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. ------------------------------------------------------------------------------ Last updated on 28 April 2020 by alex@absint.com. Copyright 2020 AbsInt. ------------------------------------------------------------------------------ An HTML version of these release notes is available at absint.com/releasenotes/compcert/20.04