CompCert release 23.10


  • Improved CSE for conditional operators.
  • Improved value analysis used 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.


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


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