CompCert 3.2

Release 3.2, 2018-01-15

Code generation and optimization

• Inline static functions that are called only once. Can be turned off by setting the "noinline" attribute on the function.
• More consistent detection and elimination of divisions by 1.
• ARM in Thumb mode: simpler instruction sequence for branch through jump table.
• ARM: support and use the "cmn" instruction.
• Issue #208: make value analysis of comparisons more conservative for dubious comparisons such as (uintptr_t) &global == 0x1234 which are undefined behavior in CompCert.

Usability

• Resurrected support for the Cygwin x86-32 port, which got lost at release 3.0.
• Support the noinline attribute on C function definitions.
• PowerPC port with Diab toolchain: support -t <target processor> option and pass it to the Diab tools.
• Clightgen tool: add -o option to specify output file.
• Pull request #192: improve the printing of Clight intermediate code so that it looks more like valid C source. (Frédéric Besson)

Bug fixing

• Issue #P25: make sure sizeof(long double) = sizeof(double) in all contexts.
• Issue #211: wrong scoping for C99 declarations within a "for" statement.
• Issues #215 and #216: updates to clightgen.

Coq and Caml development

• Pull request #191: Support Coq version 8.7.0 and 8.7.1 in addition to Coq 8.6.1. Coq 8.6 (.0) is no longer supported owing to an incompatibility with 8.7.0. (Sigurd Schneider)
• ARM code generator: refactoring of constant expansions and EABI fixups.
• Resynchronized the list of dual-licensed files given in file LICENSE and the copyright headers of the dual-licensed files.