CompCert changelog

Release 25.04

  • Improved code generation of 64-bit arithmetic for 32-bit backends
  • Improved dead-code elimination
  • Improved value analysis
  • Basic support for _Float16
  • Improved diagnostics
  • New command line options for ARM
  • Valex improvements

24.10

  • More precise value analysis
  • Improved if-conversion heuristic
  • New options
  • Various improvements for ARM & PPC

    24.04

    • Improved function prologue and epilogue code
    • CFI directives for AArch64 and RISC-V
    • Various improvements for ARM

    23.10

    • Improved common subexpression elimination for conditional operators
    • Improved constant propagation
    • Removed limit on the number of spilling rounds

    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 a3
    • 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