CompCert release 21.04
- 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
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.