diff options
-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 + |