From 0053b1aa1d26da5d1f995a603b127daf799c2da9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 21 May 2012 16:26:30 +0000 Subject: 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 --- doc/index.html | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) (limited to 'doc') 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.
  • Parmov: compilation of parallel assignments.
  • UnionFind: a persistent union-find data structure. +
  • Postorder: postorder numbering of a directed graph.

    Definitions and theorems used in many parts of the development

    @@ -102,6 +103,7 @@ See also: Memory (implementation of the memory mo See also: Memdata (in-memory representation of data).
  • Globalenvs: global execution environments.
  • Smallstep: tools for small-step semantics. +
  • Behaviors: from small-step semantics to observable behaviors of programs.
  • Determinism: determinism properties of small-step semantics.
  • Op: operators, addressing modes and their semantics. @@ -115,7 +117,7 @@ semantics. semantics and determinized semantics.
    See also: reference interpreter. -
  • Clight: a simpler version of Cmedium where expressions contain no side-effects. +
  • Clight: a simpler version of CompCert C where expressions contain no side-effects.
  • Csharpminor: low-level structured language.
  • Cminor: low-level structured @@ -200,6 +202,21 @@ code. Tailcallproof + + Function inlining + RTL to RTL + Inlining + Inliningspec + Inliningproof + + + + Postorder renumbering of the CFG + RTL to RTL + Renumber + Renumberproof + + Constant propagation RTL to RTL -- cgit v1.2.3