CompCert release 20.10

New features

  • Support for C11 _Static_assert.
  • Support for the GCC attribute used.
  • New built-in functions for all backends:
    • __builtin_nanf
    • __builtin_nansf
    • __builtin_inff
    • __builtin_inf
    • __builtin_huge_valf
    • __builtin_huge_val
  • New __builtin_constant_p that returns 1 if the argument is a constant expression, 0 otherwise.
  • New built-in functions for ARM for checking of floating point values:
    • __builtin_copysignf
    • __builtin_isnanf
    • __builtin_isnan
    • __builtin_isinff
    • __builtin_isinf
    • __builtin_isfinitef
    • __builtin_isfinite
  • RISC-V backend: Added support for __builtin_clz* and __builtin_ctz*.
  • AArch64 backend: Added support for __builtin_ctz*.
  • New option --version-file that prints the version information in a machine-readable way.

Improved diagnostics

  • Improved diagnostics for use of bit-field members in packed structs.
  • Improved diagnostics for wrong number of arguments in call to __builtin_va_start.
  • Improved diagnostics for illegal pointer arithmetic.

Other improvements

  • Introduced new error message for redefining a built-in function.
  • Eliminated known builtins whose result is ignored.
  • Improved location information for diagnostics inside switch-statements.
  • Added __builtin_sqrt as alias for __builtin_fsqrt.


  • Reset registers reserved per pragma after processing each file.