Updated for release 1.5

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

1 files changed, 31 insertions, 0 deletions

diff --git a/Changelog b/Changelog
index 004d5cb..8e253ee 100644
--- a/Changelog
+++ b/Changelog
@@ -1,3 +1,34 @@
+Release 1.5
+=========
+
+- Support for "goto" in the source language Clight.
+
+- Added small-step semantics for Clight.
+
+- Traces for diverging executions are now uniquely defined;
+  tightened semantic preservation results accordingly.
+
+- Fixed spurious compile-time error on Clight statements of the form
+  "x = f(...)" where x is a global variable.
+
+- Fixed spurious compile-time error on Clight initializers where
+  the initial value is the result of a floating-point computation
+  (e.g. "double x = 3.14159 / 2;").
+
+- Simplified the interface of the generic dataflow solver.
+
+- Reduced running time and memory requirements for the constant propagation
+  pass.
+
+- Improved the implementation of George and Appel's graph coloring heuristic:
+  runs faster, produces better results.
+
+- Revised the implementation of branch tunneling.
+
+- Improved modularization between processor-dependent and
+  processor-independent parts.
+
+
 Release 1.4.1, 2009-06-05
 =========================