Commit e62ce4ba authored by Xavier Leroy's avatar Xavier Leroy
Browse files

Update Changelog with recent changes

parent 026f65ae
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.
- 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
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment