diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-09-21 08:10:53 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-09-21 08:10:53 +0000 |
| commit | fd6bc3111af1e115fd9c8d653056393fe40715ca (patch) | |
| tree | 369a58c80898a7cdb64da7c7f9e7d1c36a9ccd45 /doc | |
| parent | 771e05d46a08d412ea05adf7b147e0291215b92b (diff) | |
Update for release 1.8
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1512 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/index.html | 17 |
1 files changed, 12 insertions, 5 deletions
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> |