From d1cdc0496d7d52e3ab91554dbf53fcc0e7f244eb Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 17 Apr 2009 13:27:48 +0000 Subject: Various clean-ups git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1033 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- doc/index.html | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) (limited to 'doc') diff --git a/doc/index.html b/doc/index.html index f300af9..a5741f5 100644 --- a/doc/index.html +++ b/doc/index.html @@ -60,7 +60,7 @@ overview papers above were written.

the Compcert Web site.

This document and the Compcert sources are -copyright 2005, 2006, 2007, 2008 Institut National de Recherche en +copyright 2005, 2006, 2007, 2008, 2009 Institut National de Recherche en Informatique et en Automatique (INRIA) and distributed under the terms of the following license.

@@ -119,7 +119,7 @@ code, control-flow graph, finitely many physical registers, infinitely many stack slots).
See also: Locations (representation of locations). -
  • LTLin: like LTL, but the CFG is +
  • LTLin: like LTL, but the CFG is replaced by a linear list of instructions with explicit branches and labels.
  • Linear: like LTLin, with explicit spilling, reloading and enforcement of calling conventions. @@ -171,6 +171,13 @@ code. RTLgenproof + + Recognition of tail calls + RTL to RTL + Tailcall + Tailcallproof + + Constant propagation RTL to RTL -- cgit v1.2.3