CompCert release 25.04

New features

  • New command-line options for ARM:
    • -midiv
      enables the generation of hardware integer division instructions for targets that only optionally support them.
    • -finline-runtime
      triggers inline expansion of all library functions for 64-bit arithmetic.
  • Added minimal syntactic support for type _Float16.
  • C99 array declarator syntax involving static is now accepted by the parser, even though this annotation is ignored during compilation.

Improved diagnostics

The diagnostics have been improved for:

  • Flexible array members in structs containing zero-width bit-fields
  • Arrays of unions containing flexible array members

Other improvements

  • Various improvements to:
    • Code generation of 64-bit arithmetic for 32-bit backends
    • Dead code elimination for 64-bit operations
    • Value analysis for unsigned comparisons
  • Improved error message for bit-field of type _Bool with size 2...8.

Fixes

  • $NNN identifiers are now escaped in x86 and ARM assembly code.
  • Fixed assertion failure in spilling for ARM functions with a large number of float arguments.

Valex

  • Support for marking input sections as removed by the linker.
  • Upon encountering an error, Valex now carries on with the rest of the checks.