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.


------------------------------------------------------------------------------
Last updated on 25 April 2025 by alex@absint.com. Copyright 2025 AbsInt.
------------------------------------------------------------------------------
An HTML version of these release notes is available at
absint.com/releasenotes/compcert/25.04