diff options
-rw-r--r-- | Changelog | 14 |
1 files changed, 13 insertions, 1 deletions
@@ -1,22 +1,34 @@ 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. + 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. Release 3.1, 2017-08-18 |