Updates in preparation for release 2.00

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

1 files changed, 16 insertions, 47 deletions

diff --git a/doc/index.html b/doc/index.html
index 1f5d3ed..adad156 100644
--- a/doc/index.html
+++ b/doc/index.html
@@ -24,7 +24,7 @@ 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.13, 2013-03-12</H3>
+<H3 align="center">Version 2.00, 2013-06-21</H3>
 
 <H2>Introduction</H2>
 
@@ -85,7 +85,6 @@ ordered types.
 semi-lattices.
 <LI> <A HREF="html/Kildall.html">Kildall</A>: resolution of dataflow
 inequations by fixpoint iteration.
-<LI> <A HREF="html/Parmov.html">Parmov</A>: compilation of parallel assignments.
 <LI> <A HREF="html/UnionFind.html">UnionFind</A>: a persistent union-find data structure.
 <LI> <A HREF="html/Postorder.html">Postorder</A>: postorder numbering of a directed graph.
 </UL>
@@ -107,6 +106,7 @@ See also: <A HREF="html/Memdata.html">Memdata</A> (in-memory representation of d
 <LI> <A HREF="html/Determinism.html">Determinism</A>: determinism properties of small-step semantics.
 <LI> <A HREF="html/Op.html"><I>Op</I></A>: operators, addressing modes and their
 semantics.
+<LI> <A HREF="html/Subtyping.html">Subtyping</A>: a solver for atomic subtyping constraints.
 </UL>
 
 <H3>Source, intermediate and target languages: syntax and semantics</H3>
@@ -131,14 +131,12 @@ code, control-flow graph, infinitely many pseudo-registers). <BR>
 See also: <A HREF="html/Registers.html">Registers</A> (representation of
 pseudo-registers).
 <LI> <A HREF="html/LTL.html">LTL</A>: location transfer language (3-address
-code, control-flow graph, finitely many physical registers, infinitely
+code, control-flow graph of basic blocks, finitely many physical registers, infinitely
 many stack slots). <BR>
 See also: <A HREF="html/Locations.html">Locations</A> (representation of
 locations) and <A HREF="html/Machregs.html"><I>Machregs</I></A> (description of processor registers).
-<LI> <A HREF="html/LTLin.html">LTLin</A>: like LTL, but the CFG is
+<LI> <A HREF="html/Linear.html">Linear</A>: like LTL, but the CFG is
 replaced by a linear list of instructions with explicit branches and labels.
-<LI> <A HREF="html/Linear.html">Linear</A>: like LTLin, with explicit
-spilling, reloading and enforcement of calling conventions.
 <LI> <A HREF="html/Mach.html">Mach</A>: like Linear, with a more concrete
 view of the activation record.  
 <LI> <A HREF="html/Asm.html"><I>Asm</I></A>: abstract syntax for PowerPC assembly
@@ -189,9 +187,11 @@ code.
   <TD>Recognition of operators<br>and addressing modes</TD>
   <TD>Cminor to CminorSel</TD>
   <TD><A HREF="html/Selection.html">Selection</A><br>
-      <A HREF="html/SelectOp.html"><I>SelectOp</I></A></TD>
+      <A HREF="html/SelectOp.html"><I>SelectOp</I></A><br>
+      <A HREF="html/SelectLong.html">SelectLong</A></TD>
   <TD><A HREF="html/Selectionproof.html">Selectionproof</A><br>
-      <A HREF="html/SelectOpproof.html"><I>SelectOpproof</I></A></TD>
+      <A HREF="html/SelectOpproof.html"><I>SelectOpproof</I></A><br>
+      <A HREF="html/SelectLongproof.html">SelectLongproof</A></TD>
 </TR>
 
 <TR valign="top">
@@ -228,7 +228,8 @@ code.
   <TD>Constant propagation</TD>
   <TD>RTL to RTL</TD>
   <TD><A HREF="html/Constprop.html">Constprop</A><br>
-      <A HREF="html/ConstpropOp.html"><I>ConstpropOp</I></A></TD>
+      <A HREF="html/ConstpropOp.html"><I>ConstpropOp</I></A><br>
+      <A HREF="html/Liveness.html">Liveness</A></TD>
   <TD><A HREF="html/Constpropproof.html">Constpropproof</A><br>
       <A HREF="html/ConstpropOpproof.html"><I>ConstproppOproof</I></A></TD>
 </TR>
@@ -243,14 +244,10 @@ code.
 </TR>
 
 <TR valign="top">
-  <TD>Register allocation by coloring<br>of an interference graph</TD>
+  <TD>Register allocation (validation a posteriori)</TD>
   <TD>RTL to LTL</TD>
-  <TD><A HREF="html/InterfGraph.html">InterfGraph</A><BR>
-      <A HREF="html/Coloring.html">Coloring</A><BR>
-      <A HREF="html/Allocation.html">Allocation</A></TD>
-  <TD><BR>
-      <A HREF="html/Coloringproof.html">Coloringproof</A><BR>
-      <A HREF="html/Allocproof.html">Allocproof</A></TD>
+  <TD><A HREF="html/Allocation.html">Allocation</A></TD>
+  <TD><A HREF="html/Allocproof.html">Allocproof</A></TD>
 </TR>
 
 <TR valign="top">
@@ -262,36 +259,19 @@ code.
 
 <TR valign="top">
   <TD>Linearization of the CFG</TD>
-  <TD>LTL to LTLin</TD>
+  <TD>LTL to Linear</TD>
   <TD><A HREF="html/Linearize.html">Linearize</A></TD>
   <TD><A HREF="html/Linearizeproof.html">Linearizeproof</A></TD>
 </TR>
 
 <TR valign="top">
   <TD>Removal of unreferenced labels</TD>
-  <TD>LTLin to LTLin</TD>
+  <TD>Linear to Linear</TD>
   <TD><A HREF="html/CleanupLabels.html">CleanupLabels</A></TD>
   <TD><A HREF="html/CleanupLabelsproof.html">CleanupLabelsproof</A></TD>
 </TR>
 
 <TR valign="top">
-  <TD>Spilling, reloading, calling conventions</TD>
-  <TD>LTLin to Linear</TD>
-  <TD><A HREF="html/Reload.html">Reload</A><BR>
-      <A HREF="html/Conventions.html">Conventions</A><BR>
-      <A HREF="html/Conventions1.html"><I>Conventions1</I></A><BR></TD>
-  <TD><A HREF="html/Parallelmove.html">Parallelmove</A><BR>
-      <A HREF="html/Reloadproof.html">Reloadproof</A></TD>
-</TR>
-
-<TR valign="top">
-  <TD>Redundant reload elimination</TD>
-  <TD>Linear to Linear</TD>
-  <TD><A HREF="html/RRE.html">RRE</A></TD>
-  <TD><A HREF="html/RREproof.html">RREproof</A></TD>
-</TR>
-
-<TR valign="top">
   <TD>Laying out the activation records</TD>
   <TD>Linear to Mach</TD>
   <TD><A HREF="html/Stacking.html">Stacking</A><BR>
@@ -313,23 +293,12 @@ code.
 <H3>Type systems</H3>
 
 Trivial type systems are used to statically capture well-formedness
-conditions on the source and intermediate languages.
+conditions on some intermediate languages.
 <UL>
 <LI> <A HREF="html/RTLtyping.html">RTLtyping</A>: typing for RTL + type
 reconstruction.
-<LI> <A HREF="html/LTLtyping.html">LTLtyping</A>: typing for LTL.
-<LI> <A HREF="html/LTLintyping.html">LTLintyping</A>: typing for LTLin.
 <LI> <A HREF="html/Lineartyping.html">Lineartyping</A>: typing for Linear.
 </UL>
-Proofs that compiler passes are type-preserving:
-<UL>
-<LI> <A HREF="html/Alloctyping.html">Alloctyping</A> (register allocation).
-<LI> <A HREF="html/Tunnelingtyping.html">Tunnelingtyping</A> (branch tunneling).
-<LI> <A HREF="html/Linearizetyping.html">Linearizetyping</A> (code linearization).
-<LI> <A HREF="html/CleanupLabelstyping.html">CleanupLabelstyping</A> (removal of unreferenced labels).
-<LI> <A HREF="html/Reloadtyping.html">Reloadtyping</A> (spilling and reloading).
-<LI> <A HREF="html/RREtyping.html">RREtyping</A> (redundant reload elimination).
-</UL>
 
 <H3>All together</H3>