Release CompCert 3.11 · AbsInt/CompCert

New features

Enumeration types are compatible only with int but not with other integer types.
Fixed confusion between unprototyped function pointer types T (*)() and prototyped, zero-argument function pointer types T (*)(void) in type casts (#431).

Improved control-flow analysis of calls to "noreturn" functions, resulting in more accurate warnings.
More detailed warning for unprototyped function definitions, now shows the prototyped type that is given to the function.
Extended the warning above to definitions of the form T f() { ... }, i.e. unprototyped but with no parameters. (Before, the warning would trigger only if parameters were declared.)
Check (and warn if requested) for arguments of struct/union types passed to a variable-argument function.

RISC-V: fixed an error in the modeling of float32 <-> float64 conversions when the argument is a NaN (#428).
x86: changed the compilation of __builtin_fmin and __builtin_fmax so that their NaN behavior is the one documented in the manual.
Improved reproducibility of register allocation. (Before, compiling CompCert with two different OCaml versions could have resulted in correct but different allocations.)
Hardened the configure script against Cygwin installations that produce \r\n for end-of-lines (#434).
RISC-V: tail calls to far-away functions were causing link-time errors (#436, #437).