Update for release 1.8

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

3 files changed, 42 insertions, 18 deletions

diff --git a/Changelog b/Changelog
index 2842d3b..cc154e2 100644
--- a/Changelog
+++ b/Changelog
@@ -1,15 +1,16 @@
-Release 1.8
-===========
+Release 1.8, 2010-09-21
+=======================
 
 - The input language to the proved part of the compiler is no longer
   Clight but CompCert C: a larger subset of the C language supporting
-  in particular side-effects within expressions.  The transformation
-  that pulls side effects out of expressions, formerly performed by
-  untrusted Caml code, is now fully proved in Coq.
+  in particular side-effects within expressions.  The transformations
+  that pull side effects out of expressions and materialize implicit
+  casts, formerly performed by untrusted Caml code, are now fully
+  proved in Coq.
 
 - New port targeting Intel/AMD x86 processors.  Generates 32-bit x86 code
   using SSE2 extensions for floating-point arithmetic.  Works under
-  Linux, *BSD, MacOS X, and the Cygwin environment for Windows.
+  Linux, MacOS X, and the Cygwin environment for Windows.
   CompCert's compilation strategy is not a very good match for the
   x86 architecture, therefore the performance of the generated code
   is not as good as for the PowerPC port, but still usable.
diff --git a/README b/README
index 29cd47f..dd81ae3 100644
--- a/README
+++ b/README
@@ -3,7 +3,7 @@
 OVERVIEW:
 
 The Compcert verified compiler is a compiler for a large subset of the
-C programming language that generates code for the PowerPC and ARM
+C programming language that generates code for the PowerPC, ARM and x86
 processors.
 
 The distinguishing feature of Compcert is that it has been formally
@@ -36,12 +36,14 @@ SUPPORTED PLATFORMS:
 - PowerPC / Linux   [somewhat experimental]
     For PowerPC machines running the Linux operating system.
 
+- IA32 / Linux or MacOS or Windows+Cygwin  [experimental]
+   For Intel/AMD x86 processors with SSE2 extensions
+   (i.e. Pentium 4 and later), running either Linux, MacOS 10.6,
+   or Windows with the Cygwin environment (http://www.cygwin.com/).
+
 - ARM / Linux       [experimental]
    For ARM machines running the Linux operating system.
 
-- IA32 / Linux, BSD, MacOS  [experimental]
-   For Intel/AMD x86 processors with SSE2 extensions
-   (i.e. Pentium 4 and later).  
 
 PREREQUISITES:
 
@@ -55,6 +57,19 @@ PREREQUISITES:
 * The Caml functional language, version 3.10 or later.
   Caml is free software, available from http://caml.inria.fr/
 
+* Under MacOS 10.5 and 10.6, some standard C include files in /usr/include/
+  contain gcc-isms that cause errors when compiling with CompCert.
+  Symptoms include:
+    - references to undefined types uint16_t and uint32_t
+    - a type error when using the "assert" macro.
+  These issues have been reported through Apple Developer's Connection.
+  Until Apple fixes them, you can apply the patch available from
+        http://compcert.inria.fr/release/MacOSX-includes.patch
+  Download this file, then do:
+     sudo /bin/bash
+     cd /
+     patch -p0 < ..../MacOSX-includes.patch
+
 
 INSTALLATION:
 
@@ -68,8 +83,8 @@ where <target> is one of:
             ppc-linux        (PowerPC, Linux)
             arm-linux        (ARM, Linux)
             ia32-linux       (x86 SSE2 32 bits, Linux)
-            ia32-bsd         (x86 SSE2 32 bits, BSD)
             ia32-macosx      (x86 SSE2 32 bits, MacOS X)
+            ia32-cygwin      (x86 SSE2 32 bits, Cygwin environment for Windows)
 
 This generates the Makefile.config file in the top directory.
 
@@ -92,8 +107,9 @@ The "configure" script accepts the following options:
 
 This re-checks all the Coq proofs, then extracts Caml code from the
 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.
+code to generate the executable for Compcert.  This step takes 20
+minutes or so on a recent machine; be patient.
+
 
 3- You can now install Compcert.  This will create the "ccomp" command
 in the binary directory selected during configuration, and install
diff --git a/doc/index.html b/doc/index.html
index 07ab0ff..67b821f 100644
--- a/doc/index.html
+++ b/doc/index.html
@@ -24,12 +24,12 @@ a:active {color : Red; text-decoration : underline; }
 
 <H1 align="center">The Compcert verified compiler</H1>
 <H2 align="center">Commented Coq development</H2>
-<H3 align="center">Version 1.7, 2010-03-31</H3>
+<H3 align="center">Version 1.8, 2010-09-21</H3>
 
 <H2>Introduction</H2>
 
-<P>Compcert is a compiler that generates PowerPC and ARM assembly
-code from Clight, a large subset of the C programming language.
+<P>Compcert is a compiler that generates PowerPC, ARM and x86 assembly
+code from Compcert C, a large subset of the C programming language.
 The particularity of this compiler is that it is written mostly within
 the specification language of the Coq proof assistant, and its
 correctness --- the fact that the generated assembly code is
@@ -104,7 +104,7 @@ semantics.
 <H3>Source, intermediate and target languages: syntax and semantics</H3>
 
 <UL>
-<LI> The Cmedium source language:
+<LI> The Compcert C source language:
 <A HREF="html/Csyntax.html">syntax</A> and
 <A HREF="html/Csem.html">semantics</A> and
 <A HREF="html/Cstrategy.html">determinized semantics</A>.
@@ -149,7 +149,7 @@ code.
 <TR valign="top">
   <TD>Pulling side-effects out of expressions;<br>
       fixing an evaluation order</TD>
-  <TD>Cmedium to Clight</TD>
+  <TD>Compcert C to Clight</TD>
   <TD><A HREF="html/SimplExpr.html">SimplExpr</A></TD>
   <TD><A HREF="html/SimplExprspec.html">SimplExprspec</A><br>
       <A HREF="html/SimplExprproof.html">SimplExprproof</A></TD>
@@ -211,6 +211,13 @@ code.
 </TR>
 
 <TR valign="top">
+  <TD>Elimination of redundant casts</TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/CastOptim.html">CastOptim</A></TD>
+  <TD><A HREF="html/CastOptimproof.html">CastOptimproof</A></TD>
+</TR>
+
+<TR valign="top">
   <TD>Register allocation by coloring<br>of an interference graph</TD>
   <TD>RTL to LTL</TD>
   <TD><A HREF="html/InterfGraph.html">InterfGraph</A><BR>