powerpc/PrintAsm.ml arm/PrintAsm.ml: updated (no label elimination).

Added -dmach option and corresponding printer for Mach code.
CleanupLabelsproof.v: fixed for ARM
Driver.ml: -E sends output to stdout; support for .s and .S source files.
cparser/Elab.ml: spurious comment deleted.


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

1 files changed, 26 insertions, 0 deletions

diff --git a/Changelog b/Changelog
index bf4a65b9..25400a7c 100644
--- a/Changelog
+++ b/Changelog
@@ -1,3 +1,29 @@
+- Support for "aligned" attributes on global variables, e.g.
+    __attribute__((aligned(16))) int x;
+
+- Pointer comparisons now treated as unsigned comparisons (previously: signed).
+  This fixes an issue with arrays straddling the 0x8000_0000 boundary.
+  Consequently, the "ofs" part of pointer values "Vptr b ofs" is
+  now treated as unsigned (previously: signed).
+
+- Elimination of unreferenced labels now performed by a separate pass
+  (backend/CleanupLabels.v) and proved correct.
+
+- Stacking pass revised: supports more flexible layout of the stack
+  frame; two-step proof (Stackingproof + Machabstr2concr) merged
+  into one single proof (Stackingproof).
+
+- The requirement that pointers be valid in pointer comparisons
+  was pushed through all intermediate languages of the back-end
+  (previously: requirement present only in up to Csharpminor).
+
+- Improvements to the compiler driver:
+    .  -E option now prints preprocessed result to standard output
+       instead of saving it in a .i file
+    .  support for .s (assembly) and .S (assembly to be preprocessed)
+       input files
+
+
 Release 1.8.1, 2011-03-14
 =========================