Release CompCert 3.15 · AbsInt/CompCert

C language support

Minimal syntactic support for _Float16 type (half-precision FP numbers). Function declarations using _Float16 are correctly parsed, but any actual use of _Float16 is rejected later during compilation. (#525)
Support C99 array declarator syntax involving static and *. These annotations are correctly parsed, but ignored during typing and compilation. (#539)

Better support for _Bool type in the back-end and in the memory model.
This avoids redundant normalizations to _Bool.
Take types of function parameters into account during value analysis.
This avoids redundant normalizations on parameters of small integer types.
More conservative static analysis of pointer comparisons. (#516)
Refined heuristic for if-conversion. Turn if-conversion off in some cases where it would prevent later optimization of conditional branches in the continuation of the if.
CSE: remember pointer alias information in Load equations, making it possible to remove more redundant memory loads. (#518)
More precise value analysis of integer multiplication, division, modulus.
Constant propagation: optimize "known integer or undefined" results. For example, &x == &x, which is either 1 or undefined, is now replaced by 1.
Optimize (x ^ cst) != 0 into x != cst.
Avoid quadratic compile-time behavior on deeply-nested if statements. (#519)

More robust determination of symbols that may be defined in a shared object. (#538)
Escape $NNN identifiers in generated x86 and ARM assembly code (#541).
Wrong parameter scoping in function definitions such as int (*f(int y))(int x) { ... } (a function returning a pointer to a prototyped function).

Mark stack as non-executable in binaries produced by ccomp.
Check that preprocessed sources (.i files) do not contain backslash-newline sequences.
./configure arm-linux now selects the hard-FP ABI, since Linux distributions no longer use the soft-FP ABI.