diff options
-rw-r--r-- | doc/index.html | 13 |
1 files changed, 5 insertions, 8 deletions
diff --git a/doc/index.html b/doc/index.html index aa1847f5..1f5d3ed5 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.12, 2013-01-11</H3> +<H3 align="center">Version 1.13, 2013-03-12</H3> <H2>Introduction</H2> @@ -140,8 +140,7 @@ 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. <BR> -See also: <A HREF="html/Machsem.html">Machsem</A> operational semantics for Mach. <BR> +view of the activation record. <LI> <A HREF="html/Asm.html"><I>Asm</I></A>: abstract syntax for PowerPC assembly code. </UL> @@ -298,15 +297,15 @@ code. <TD><A HREF="html/Stacking.html">Stacking</A><BR> <A HREF="html/Bounds.html">Bounds</A><BR> <A HREF="html/Stacklayout.html"><I>Stacklayout</I></A></TD> - <TD><A HREF="html/Stackingproof.html">Stackingproof</A><BR> - <A HREF="html/Asmgenretaddr.html"><I>Asmgenretaddr</I></A></TD> + <TD><A HREF="html/Stackingproof.html">Stackingproof</A></TD> </TR> <TR valign="top"> <TD>Emission of assembly code</TD> <TD>Mach to Asm</TD> <TD><A HREF="html/Asmgen.html"><I>Asmgen</I></A></TD> - <TD><A HREF="html/Asmgenproof1.html"><I>Asmgenproof1</I></A><BR> + <TD><A HREF="html/Asmgenproof0.html"><I>Asmgenproof0</I></A><BR> + <A HREF="html/Asmgenproof1.html"><I>Asmgenproof1</I></A><BR> <A HREF="html/Asmgenproof.html"><I>Asmgenproof</I></A></TD> </TR> </TABLE> @@ -321,7 +320,6 @@ 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. -<LI> <A HREF="html/Machtyping.html">Machtyping</A>: typing for Mach. </UL> Proofs that compiler passes are type-preserving: <UL> @@ -331,7 +329,6 @@ Proofs that compiler passes are type-preserving: <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). -<LI> <A HREF="html/Stackingtyping.html">Stackingtyping</A> (layout of activation records). </UL> <H3>All together</H3> |