Pointers one past

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

1 files changed, 3 insertions, 1 deletions

diff --git a/Changelog b/Changelog
index 81429ef..243cdff 100644
--- a/Changelog
+++ b/Changelog
@@ -7,7 +7,9 @@ Development version
   reductions to be incorrectly merged.
 - Better error and warning messages for declarations of variables
   of size >= 2^32 bits.
-
+- Comparisons involving pointers "one past" the end of a block are
+  now defined.  (They used to be undefined behavior.)
+  (Contributed by Robbert Krebbers).
 
 Release 1.12.1, 2013-01-29
 ==========================