Updates for release 1.7

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

2 files changed, 64 insertions, 9 deletions

diff --git a/Changelog b/Changelog
index 750048d..45dd53d 100644
--- a/Changelog
+++ b/Changelog
@@ -1,3 +1,49 @@
+Release 1.7, 2010-03-31
+=======================
+
+- New implementation of the C type-checker, simplifier, and translation to
+  Clight.  Compared with the previous CIL-based solution, the new
+  implementation is more modular and supports more optional simplifications.
+
+- More features of the C language are handled by expansion during
+  translation to Clight:
+    . assignment between structs and unions (option -fstruct-assign)
+    . passing structs and union by value (option -fstruct-passing)
+    . bit-fields in structs (option -fbitfields)
+
+- The "volatile" modifier is now honored.  Volatile accesses are represented
+  in Clight by calls to built-in functions, which are preserved throughout
+  the compilation chain, then turned into processor loads and stores
+  at the end.
+
+- Generic support for C built-in functions.  These predefined external
+  functions give access to special instructions of the processor.  See
+  powerpc/CBuiltins.ml for the list of PowerPC built-in functions.
+
+- The memory model now exposes the bit-level in-memory representation
+  of integers and floats.  This strengthens the semantic preservation
+  theorem: we now prove that C code that directly manipulates these
+  bit-level representations (e.g. via a union between floats and integers)
+  is correctly compiled.
+
+- The memory model now supports fine-grained access control to individual
+  bytes of a memory block.  This feature is currently unused in the 
+  compiler proofs, but will facilitate connections with separation logics
+  later.
+
+- External functions are now allowed to read and modify memory.
+  The semantic preservation proofs were strengthened accordingly.
+  In particular, this enables the malloc() and free() C library functions
+  to be modeled as external functions in a provably correct manner.
+
+- Minor improvements in the handling of global environments and the
+  construction of the initial memory state.
+
+- Bug fixes in the handling of '#pragma section' and '#pragma set_section'.
+
+- The C test suite was enriched and restructured.
+
+	
 Release 1.6, 2010-01-13
 =======================
 
diff --git a/README b/README
index 42f0443..44a845e 100644
--- a/README
+++ b/README
@@ -19,7 +19,7 @@ purposes.
 COPYRIGHT:
 
 The Compcert verified compiler is Copyright 2004, 2005, 2006, 2007,
-2008, 2009 Institut National de Recherche en Informatique et en
+2008, 2009, 2010 Institut National de Recherche en Informatique et en
 Automatique (INRIA).  It is distributed under the conditions stated in
 file LICENSE.
 
@@ -27,7 +27,7 @@ file LICENSE.
 SUPPORTED PLATFORMS:
 
 - PowerPC / MacOS   [stable]
-    For Apple Macs running the MacOS 10.4 or 10.5 operating system.
+    For Apple Macs running the MacOS 10.4, 10.5 or 10.6 operating system.
     Both PowerPC-based and Intel-based Macs are supported.
     The PowerPC code generated by the Compcert compiler runs
     natively at full speed on PowerPC-based Macs, and runs under
@@ -65,8 +65,7 @@ where <target> is one of:
             ppc-linux        (PowerPC, Linux)
             arm-linux        (ARM, Linux)
 
-This generates the Makefile.config file in the top directory
-and prepares and configures the CIL library in the cil/ subdirectory.
+This generates the Makefile.config file in the top directory.
 
 The "configure" script accepts the following options:
 
@@ -85,9 +84,9 @@ The "configure" script accepts the following options:
              make all
 
 This re-checks all the Coq proofs, then extracts Caml code from the
-Coq specification and combines it with the CIL library and supporting
-hand-written Caml code to generate the executable for Compcert.  This
-step takes 10 to 15 minutes on a recent Mac computer; be patient.
+Coq specification and combines it with supporting hand-written Caml
+code to generate the executable for Compcert.  This step takes 10 to
+15 minutes on a recent Mac computer; be patient.
 
 3- You can now install Compcert.  This will create the "ccomp" command
 in the binary directory selected during configuration, and install
@@ -142,8 +141,18 @@ Preprocessing options:
   -I<dir>        Add <dir> to search path for #include files
   -D<symb>=<val> Define preprocessor symbol
   -U<symb>       Undefine preprocessor symbol
-Compilation options:
-  -flonglong     Treat 'long long' as 'long' and 'long double' as 'double'
+Language support options (use -fno-<opt> to turn off -f<opt>) :
+  -fbitfields    Emulate bit fields in structs [off]
+  -flonglong     Treat 'long long' as 'long' and 'long double' as 'double' [off]
+  -fstruct-passing  Emulate passing structs and unions by value [off]
+  -fstruct-assign   Emulate assignment between structs or unions [off]
+  -fvararg-calls Emulate calls to variable-argument functions [on]
+Code generation options:
+  -fmadd         Use fused multiply-add and multiply-sub instructions
+  -fsmall-data <n>  Set maximal size <n> for allocation in small data area
+  -fsmall-const <n>  Set maximal size <n> for allocation in small constant area
+Tracing options:
+  -dparse        Save C file after parsing and elaboration in <file>.parse.c
   -dclight       Save generated Clight in <file>.light.c
   -dasm          Save generated assembly in <file>.s
 Linking options: