CompCert release 23.10


  • Improved common subexpression elimination for conditional operators.
  • Improved value analysis for constant propagation.
  • Use movl instruction for loading unsigned 32-bit integer constants for x86-64.
  • Removed the limit on the number of spilling rounds that are performed.
  • Improved error message for integer literals that are too large for signed types.
  • Reordered emitted constants inside code to avoid excessively large offsets for floating-point constants.
  • Avoid using fld/fsd for built-in memcpy for RISC-V for -fno-fpu.


Updated the API for Valex QSK eval runs to maintain success status flags of their own rather than relying on the return value of the main evaluation function.