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

● Improved speed for large code sizes.

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

Last updated on 26 April 2023 by Copyright 2023 AbsInt.
An HTML version of these release notes is available at