Floats.v, Nan.v: hard-wire the general shape of binop_pl, so that no axioms

are necessary, only two parameters (default_pl and choose_binop_pl).
SelectDiv: optimize FP division by a power of 2.
ConstpropOp: optimize 2.0 * x and x * 2.0 into x + x.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2326 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 5 insertions, 0 deletions

diff --git a/Changelog b/Changelog
index 5f0c7c7..b603c32 100644
--- a/Changelog
+++ b/Changelog
@@ -5,8 +5,13 @@ Development trunk:
   arithmetic.
 - Optimize integer divisions by positive constants, turning them into
   multiply-high and shifts.
+- Optimize floating-point divisions by powers of 2, turning them
+  into multiplications.
+- Optimize "x * 2.0" and "2.0 * x" into "x + x".
 - Avoid double rounding issues in conversion from 64-bit integers
   to single-precision floats.
+- Fixed typing rules for __builtin_annot() to avoid casting arguments
+  of small integer or FP types.
 - PowerPC: more efficient implementation of division on 64-bit integers.
 - Minor simplifications in the generic solvers for dataflow analysis.