Updated for version 1.13

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

1 files changed, 22 insertions, 10 deletions

diff --git a/Changelog b/Changelog
index 5bf7335..65a7236 100644
--- a/Changelog
+++ b/Changelog
@@ -1,24 +1,36 @@
-Development version
-===================
+Release 1.13, 2013-03-12
+========================
 
-- More efficient implementation of machine integers (module Integers)
-  taking advantage of bitwise operations defined in ZArith in Coq 8.4.
-- Fixed a bug in the reference interpreter in -all mode causing some
-  reductions to be incorrectly merged.
-- Better error and warning messages for declarations of variables
-  of size >= 2^32 bits.
+Language semantics:
 - Comparisons involving pointers "one past" the end of a block are
   now defined.  (They used to be undefined behavior.)
   (Contributed by Robbert Krebbers).
+
+Language features:
 - Arguments to __builtin_annot() that are compile-time constants
   are now replaced by their (integer or float) value in the annotation
   generated in the assembly file.
+
+Improvements in performance:
 - ARM and PowerPC ports: more efficient access to function parameters
   that are passed on the call stack.
 - ARM port; slightly better code generated for some indirect memory
   accesses.
-- Coq cleanups: a number of definitions that were opaque for no good reason
-  are now properly transparent.
+
+Improvements in usability:
+- Better error and warning messages for declarations of variables
+  of size >= 2^32 bits.
+- Fixed a bug in the reference interpreter in -all mode causing some
+  reductions to be incorrectly merged.
+- Reference interpreter: more efficient exploration of states in -all mode.
+
+Coq development:
+- More efficient implementation of machine integers (module Integers)
+  taking advantage of bitwise operations defined in ZArith in Coq 8.4.
+- Revised handling of return addresses in the Mach language
+  and the Stacking and Asmgen passes.
+- A number of definitions that were opaque for no good reason are now
+  properly transparent.
 
 
 Release 1.12.1, 2013-01-29