Release CompCert 3.13 · AbsInt/CompCert

Code generation and optimization:

Slightly more precise value analysis, with a better distinction between "any integer value" and "any integer or pointer value". (#490)
Recognize a few more nested conditional expressions that can be if-converted into a conditional move.
Register allocation: better support for "preferred" registers, e.g. registers R0-R3 on ARM Thumb, which enable more compact instruction encodings.
ARM Thumb: use more instructions that can be encoded in 16 bits, producing more compact code.
x86: use a shorter instruction encoding for loading unsigned 32-bit constants. (#487)

_Noreturn on function definitions (but not declarations) was ignored sometimes.
The argument of __builtin_va_end was discarded, is now evaluated for its side effects.
Tail call optimization must be disabled in variadic functions, otherwise a va_list structure can get out of scope.
Nested compound initializers were elaborated in the wrong order, causing compile-time failures later in the compilation pipeline.
The signedness of a bit field was determined differently when its type was an enum type and when it was a typedef to an enum type.

Define wchar_t exactly like the ABI says. On most platforms, CompCert was defining wchar_t as signed int, but it must be unsigned int for AArch64-ELF and unsigned long for PowerPC-EABI.

Removed support for Cygwin 32 bits, which has reached end of life. Cygwin 64 bits remains supported.

Support Coq 8.16.0 and 8.16.1, addressing most of the new warnings in 8.16.
When installing the Coq development, also install coq-native generated files.
Tweak some proof scripts for compatibility with future Coq versions. (#465, #470, #491, #492)
Updated the vendored copy of Flocq to version 4.1.1.