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.

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

Last updated on 26 April 2021 by Copyright 2021 AbsInt.
An HTML version of these release notes is available at