From b8e535ccf82385573f80f6d146c04892b25ea0a6 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 28 Jul 2014 12:06:06 +0000 Subject: Updated Changelog git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2552 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- Changelog | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/Changelog b/Changelog index 24f4225..604618c 100644 --- a/Changelog +++ b/Changelog @@ -1,3 +1,31 @@ +- Revised and improved support for single-precision floating-point + arithmetic. Earlier, all FP arithmetic was performed at double + precision, with conversions to/from single precision as needed, + in particular when loading/storing a single-precision FP number + from/to memory. Now, FP operations whose arguments are of type + "float" are performed in single-precision, using the processor's + single FP instructions. Fewer conversions between double and + single precision are generated. + +- Refactored the library of FP arithmetic (lib/Floats.v) to support + both 64- and 32-bit floats. +- Some more theorems proved about float<->integer conversions. + +- ARM port: added support for Thumb2 instruction encoding (option -fthumb). + Thumb2 is supported on ARMv7 and up, and produces more compact + machine code. + +- The memory model was extended with two new "chunks", Many32 and Many64, + that enable storing any 32-bit value or 64-bit value using + an opaque, not bit-based encoding, and reloading these values exactly. + These new chunks are used to implement saving and restoring callee-save + registers that can contain data of unknown types (e.g. float32 or float64) + but known sizes. + + +Release 2.3pl2, 2014-05-15 +========================== + Usability: - Re-added support for "__func__" identifier as per ISO C99. - Re-added some popular GCC extensions to ISO C99: -- cgit v1.2.3