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 == 0x1234which are undefined behavior in CompCert.
Usability
- Resurrected support for the Cygwin x86-32 port, which got lost at release 3.0.
- Support the
noinlineattribute on C function definitions. - PowerPC port with Diab toolchain: support
-t <target processor>option and pass it to the Diab tools. - Clightgen tool: add
-ooption 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.