CompCert changelog

Current release 23.04

  • Support for Duff’s Device
  • Support for Unicode character constants and string literals
  • Improved instruction selection and register allocation for ARM/Thumb

22.10

  • Support for C11 _Generic selection
  • Improved if-conversion optimization
  • Mergeable string and literal sections

22.04

  • Formally verified handling of bitfields in structs and unions
  • Support for producing Csyntax abstract syntax

21.10

  • Support for non-integer bitfields
  • Support for 32-bit PowerPC VLE with the NXP-GCC toolchain
  • Extended inline assembly

21.04

  • Improved ABI compatibility
  • Improved diagnostics
  • Additional and improved built-ins

20.10

  • New built-in functions
  • Improved diagnostics
  • Support for _Static_assert

20.04

  • New architecture AArch64
  • Improved error messages
  • Improved DWARF support

19.10

  • If-conversion optimization
  • Improved built-in functions
  • New diagnostics

19.04

  • Improved attribute handling
  • Improved scoping
  • Improved DWARF handling

18.10

  • Better handling of _Alignof/_Alignas
  • Valex check for symbol placement
  • New diagnostics

18.04

  • New builtin for integration with ał
  • JSON export of ARM assembly
  • Valex for ARM

17.10

  • New backend for hybrid 64-/32-bit PPC
  • New compiler optimizations
  • Qualification Support Kit for Valex

17.04

  • Full support for C11 anonymous compound types
  • Checks for unused variables and parameters

16.10

  • Improved support for K&R, ARM and PowerPC
  • Compatibility with coq v8.5pl2

16.04

  • New options for GCC compatibility
  • More built-in functions
  • Various fixes

15.10

  • Valex tool
  • DWARF2 support
  • New language features