summaryrefslogtreecommitdiff
path: root/doc/index.html
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2010-08-18 09:06:55 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2010-08-18 09:06:55 +0000
commita15858a0a8fcea82db02fe8c9bd2ed912210419f (patch)
tree5c0c19439f0d0f9e8873ce0dad2034cb9cafc4ba /doc/index.html
parentadedca3a1ff17ff8ac66eb2bcd533a50df0927a0 (diff)
Merge of branches/full-expr-4:
- Csyntax, Csem: source C language has side-effects within expressions, performs implicit casts, and has nondeterministic reduction semantics for expressions - Cstrategy: deterministic red. sem. for the above - Clight: the previous source C language, with pure expressions. Added: temporary variables + implicit casts. - New pass SimplExpr to pull side-effects out of expressions (previously done in untrusted Caml code in cparser/) - Csharpminor: added temporary variables to match Clight. - Cminorgen: adapted, removed cast optimization (moved to back-end) - CastOptim: RTL-level optimization of casts - cparser: transformations Bitfields, StructByValue and StructAssign now work on non-simplified expressions - Added pretty-printers for several intermediate languages, and matching -dxxx command-line flags. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1467 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'doc/index.html')
-rw-r--r--doc/index.html25
1 files changed, 17 insertions, 8 deletions
diff --git a/doc/index.html b/doc/index.html
index dff66ce..07ab0ff 100644
--- a/doc/index.html
+++ b/doc/index.html
@@ -104,8 +104,11 @@ semantics.
<H3>Source, intermediate and target languages: syntax and semantics</H3>
<UL>
-<LI> <A HREF="html/Csyntax.html">Clight syntax</A> and its
-<A HREF="html/Csem.html">semantics</A>: the source language.
+<LI> The Cmedium 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>.
+<LI> <A HREF="html/Clight.html">Clight</A>: a simpler version of Cmedium where expressions contain no side-effects.
<LI> <A HREF="html/Csharpminor.html">Csharpminor</A>: low-level
structured language.
<LI> <A HREF="html/Cminor.html">Cminor</A>: low-level structured
@@ -144,13 +147,20 @@ code.
</TR>
<TR valign="top">
+ <TD>Pulling side-effects out of expressions;<br>
+ fixing an evaluation order</TD>
+ <TD>Cmedium 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>
+</TR>
+<TR valign="top">
<TD>Simplification of control structures; <br>
explication of type-dependent computations</TD>
<TD>Clight to Csharpminor</TD>
<TD><A HREF="html/Cshmgen.html">Cshmgen</A></TD>
- <TD><A HREF="html/Cshmgenproof1.html">Cshmgenproof1</A><br>
- <A HREF="html/Cshmgenproof2.html">Cshmgenproof2</A><br>
- <A HREF="html/Cshmgenproof3.html">Cshmgenproof3</A></TD>
+ <TD><A HREF="html/Cshmgenproof.html">Cshmgenproof</A></TD>
+</TR>
<TR valign="top">
<TD>Stack allocation of local variables<br>
whose address is taken;<br>
@@ -263,7 +273,6 @@ code.
Trivial type systems are used to statically capture well-formedness
conditions on the source and intermediate languages.
<UL>
-<LI> <A HREF="html/Ctyping.html">Ctyping</A>: partial typing for Clight + type-checking
<LI> <A HREF="html/RTLtyping.html">RTLtyping</A>: typing for RTL + type
reconstruction.
<LI> <A HREF="html/LTLtyping.html">LTLtyping</A>: typing for LTL.
@@ -283,8 +292,8 @@ Proofs that compiler passes are type-preserving:
<H3>All together</H3>
<UL>
-<LI> <A HREF="html/Compiler.html">Compiler</A>: composing the passes together; the
-final semantic preservation theorems.
+<LI> <A HREF="html/Compiler.html">Compiler</A>: composing the passes together;
+whole-compiler semantic preservation theorems.
<LI> <A HREF="html/Complements.html">Complements</A>: interesting consequences of the semantic preservation theorems.
</UL>