From e62ce4ba961cd0767a80f9e89f6f559bc1e341e9 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 11 Jan 2018 15:10:04 +0100 Subject: Update Changelog with recent changes --- Changelog | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) (limited to 'Changelog') diff --git a/Changelog b/Changelog index 0a45e468..9b471b9c 100644 --- a/Changelog +++ b/Changelog @@ -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 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 -- cgit