CompCert release 21.04

New features

  • New option -main to specify the entry point function in interpreter mode.
  • New diagnostic for taking the address of a built-in function.
  • Added formal semantics for some PowerPC and ARM built-ins.
  • Added built-in fmin/fmax for AArch64.

Other improvements

  • Improved diagnostic for unsupported pragmas in function bodies.
  • Improved diagnostics for unknown built-ins.
  • Modeling of registers for destroyed by pseudo-instructions.


  • Improved ABI compatibility for RISC-V.
  • Improved ABI compatibility for x86_32 struct passing.
  • Improved ABI support for variable argument functions for PowerPC.
  • Valex no longer checks variables that only have external linkage and no initializer per compilation unit. If the variable is not defined within any compilation unit it will now include the variable in the list of missing symbols.