CompCert release 23.04

New features

  • Support for Duff’s Device and other unstructured switch statements.
  • Support for Unicode character constants and string literals.
  • New command-line switch -std=<standard>.

Improved warnings

  • Improved the precision of warnings for functions with _Noreturn.
  • Improved warning for non-linear conditional expressions.

Other improvements

  • Improved instruction selection to use more Thumb instructions.
  • Improved instruction selection for load/store operations with immediate offsets for the ARM backend.
  • Changed register allocation for Thumb mode to prefer the Thumb registers (r0 - r7).
  • Enabled CSE optimization for address and integer constants for the ARM backend.
  • Improved register constraints for integer division for ARM in Thumb mode.
  • Improved if-conversion for some special cases.
  • The driver program to run QSK packages has been renamed to qualify.
  • Now using the .data.rel.ro section for const data with relocatable inits for AArch64, ARM, RISC-V and x86 ELF.
  • Now emitting the appropriate attribute Tag_ABI_VFP for the calling conventions used.

Valex

Improved speed for large code sizes.

Fixes

  • Fixed an issue with the re-usage of temporary variables in the frontend translation to avoid typing problems in later translation phases.
  • Fixed problems with Windows newlines when printing intermixed C and assembly code.