From 82d24661bf10875afa1a56868ef87649623a4687 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Thu, 27 Aug 2009 09:47:59 +0000
Subject: Updated for release 1.5

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1141 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 Changelog | 31 +++++++++++++++++++++++++++++++
 README    |  4 ++--
 2 files changed, 33 insertions(+), 2 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
 =========================
 
diff --git a/README b/README
index 3b136a9..42f0443 100644
--- a/README
+++ b/README
@@ -46,7 +46,7 @@ PREREQUISITES:
   the search path.  For MacOS X, you can get them by installing the
   XCode development tools, as found on the installation DVDs.
 
-* The Coq proof assistant, version 8.1pl3.
+* The Coq proof assistant, version 8.2-1 or later.
   Coq is free software, available from http://coq.inria.fr/
 
 * The Caml functional language, version 3.10 or later.
@@ -121,7 +121,7 @@ The generated assembly code is left in file src1.s
 The subset of the C language accepted by Compcert is quite large.
 The main features of C that are not supported are:
   - The "long long" and "long double" types.
-  - The "goto" statement, and non-structured forms of the "switch" statement.
+  - Non-structured forms of the "switch" statement (Duff's device).
   - Variable-argument functions.
 The "ccomp" command will issue errors and diagnostics if it encounters
 a C construct that it cannot process.
-- 
cgit v1.2.3