diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2018-01-11 15:10:04 +0100 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2018-01-11 15:10:04 +0100 |
commit | e62ce4ba961cd0767a80f9e89f6f559bc1e341e9 (patch) | |
tree | 9f27b2aed111d1e251a234773424145dc8a6c799 | |
parent | 026f65aebdce67b12f8ac2beebce7358d4fa2de6 (diff) | |
download | compcert-e62ce4ba961cd0767a80f9e89f6f559bc1e341e9.tar.gz compcert-e62ce4ba961cd0767a80f9e89f6f559bc1e341e9.zip |
Update Changelog with recent changes
-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 |