CompCert release 21.10

New features

  • Support for 32-bit PowerPC VLE with the NXP-GCC toolchain.
  • Support for floating-point register constraints for inputs and outputs in GCC-style extended inline assembly for AArch64, PowerPC, PowerPC VLE, RISC-V, and x86.
  • Support for the attribute weak to emit symbols as weak for elf targets.
  • Support for bitfields of types other than int, provided that they are no larger than 32 bits.
  • New built-in functions __builtin_nans and __builtin_nansf.
  • Initial frontend support for __builtin_expect and __builtin_unreachable.
  • New diagnostic for invalid initializer of flexible array member.
  • Support for "#line 0 ..." directives emitted by the GCC 11 preprocessor.

Fixes

Unnamed non bit-field members that are not allowed in C are no longer taken into account for GCC compatibility in the layout of structs or unions. Instead, CompCert now generates a warning for them.