Merge of the newmem branch:

- Revised memory model with Max and Cur permissions, but without bounds
- Constant propagation of 'const' globals
- Function inlining at RTL level
- (Unprovable) elimination of unreferenced static definitions


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

1 files changed, 18 insertions, 1 deletions

diff --git a/doc/index.html b/doc/index.html
index f767b2a..2abb967 100644
--- a/doc/index.html
+++ b/doc/index.html
@@ -87,6 +87,7 @@ semi-lattices.
 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>
 
 <H3>Definitions and theorems used in many parts of the development</H3>
@@ -102,6 +103,7 @@ See also: <A HREF="html/Memory.html">Memory</A> (implementation of the memory mo
 See also: <A HREF="html/Memdata.html">Memdata</A> (in-memory representation of data).
 <LI> <A HREF="html/Globalenvs.html">Globalenvs</A>: global execution environments.
 <LI> <A HREF="html/Smallstep.html">Smallstep</A>: tools for small-step semantics.
+<LI> <A HREF="html/Behaviors.html">Behaviors</A>: from small-step semantics to observable behaviors of programs.
 <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.
@@ -115,7 +117,7 @@ semantics.
 <A HREF="html/Csem.html">semantics</A> and
 <A HREF="html/Cstrategy.html">determinized semantics</A>.<BR>
 See also: <A HREF="html/Cexec.html">reference interpreter</A>.
-<LI> <A HREF="html/Clight.html">Clight</A>: a simpler version of Cmedium where expressions contain no side-effects.
+<LI> <A HREF="html/Clight.html">Clight</A>: a simpler version of CompCert C 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
@@ -201,6 +203,21 @@ code.
 </TR>
 
 <TR valign="top">
+  <TD>Function inlining</TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/Inlining.html">Inlining</A></TD>
+  <TD><A HREF="html/Inliningspec.html">Inliningspec</A>
+      <A HREF="html/Inliningproof.html">Inliningproof</A></TD>
+</TR>
+
+<TR valign="top">
+  <TD>Postorder renumbering of the CFG</TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/Renumber.html">Renumber</A></TD>
+  <TD><A HREF="html/Renumberproof.html">Renumberproof</A></TD>
+</TR>
+
+<TR valign="top">
   <TD>Constant propagation</TD>
   <TD>RTL to RTL</TD>
   <TD><A HREF="html/Constprop.html">Constprop</A><br>