diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-03-11 09:40:40 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-03-11 09:40:40 +0000 |
commit | 7dd08351a9167f99c04f47042fb83c03e10d5552 (patch) | |
tree | 3b89755b42f4636e90b308dbe4016dfde1c9f9af | |
parent | 617a3e0b1adf2869efa097829230da7166a7eefe (diff) |
Updated for version 1.13
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2143 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rw-r--r-- | Changelog | 32 | ||||
-rw-r--r-- | VERSION | 3 |
2 files changed, 24 insertions, 11 deletions
@@ -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 @@ -1,2 +1,3 @@ -1.12 +1.13 + |