Constant propagation within __builtin_annot.

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

1 files changed, 4 insertions, 0 deletions

diff --git a/Changelog b/Changelog
index 243cdff..cfb516d 100644
--- a/Changelog
+++ b/Changelog
@@ -10,6 +10,10 @@ Development version
 - Comparisons involving pointers "one past" the end of a block are
   now defined.  (They used to be undefined behavior.)
   (Contributed by Robbert Krebbers).
+- 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.
+
 
 Release 1.12.1, 2013-01-29
 ==========================