From 7a614ea53948423b0266eefd98ea5714559c3cfc Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 28 Jun 2012 11:23:52 +0000 Subject: Changelog: updated driver/Interp.ml: clean up dead code lib/Integers.v: add shifted_or_is_add lib/Floats.v: add from_words_eq .depend: updated git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1940 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- Changelog | 38 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) (limited to 'Changelog') diff --git a/Changelog b/Changelog index c63dc66..f07154c 100644 --- a/Changelog +++ b/Changelog @@ -1,4 +1,12 @@ +Release 1.11 +======================== + +Improvements in confidence: +- Floating-point numbers and arithmetic operations, previously axiomatized, + are now implemented and proved correct in Coq, using the Flocq library + of S. Boldo and G. Melquiond. +Language semantics: - In accordance with ISO C standards, the signed division min_int / -1 and the signed remainder min_int % -1 (where min_int is the smallest representable signed integer) now have undefined semantics and are @@ -7,6 +15,36 @@ but this behavior requires unnatural code to be generated on IA32 and PowerPC.) +Performance improvements: +- Function inlining is now implemented. The functions that are inlined + are those declared "inline" in the C source, provided they are not + recursive. +- Constant propagation is now able to propagate the initial values of + "const" global variables. +- Added option -ffloat-const-prop to control the propagation of + floating-point constants; see user's manual for documentation. +- Common subexpression elimination can now eliminate memory loads + following a memory store at the same location. +- ARM: make use of the "fcmpzd" and "fmdrr" instructions. + +New tool: +- The "cchecklink" tool performs a posteriori validation of the + assembling and linking phases. It is available for PowerPC-EABI + only. It takes as inputs an ELF-PowerPC executable as produced + by the linker, as well as .sdump files (abstract assembly) as + produced by "ccomp -sdump", and checks that the executable contains + properly-assembled and linked code and data corresponding to those + produced by CompCert. + +Other changes: +- Elimination of "static" functions and global variables that are unused. +- The memory model was enriched with "max" permissions in addition to + "current" permissions, to better reason over "const" blocks and + already-deallocated blocks. +- More efficient implementation of the memory model, resulting + in faster interpretation of source files by "ccomp -interp". + + Release 1.10, 2012-03-13 ======================== -- cgit v1.2.3