From 03b8970a778a0f4985dc44722b3dffd2a0cef73f Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 28 Aug 2009 12:46:09 +0000 Subject: Last updates for release 1.5. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1142 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- doc/index.html | 24 ++++++++++++++++-------- 1 file changed, 16 insertions(+), 8 deletions(-) (limited to 'doc') diff --git a/doc/index.html b/doc/index.html index 47c849e..88151d1 100644 --- a/doc/index.html +++ b/doc/index.html @@ -24,7 +24,7 @@ a:active {color : Red; text-decoration : underline; }

The Compcert verified compiler

Commented Coq development

-

Version 1.4, 2009-04-21

+

Version 1.5, 2009-08-28

Introduction

@@ -83,9 +83,10 @@ semi-lattices.
  • Kildall: resolution of dataflow inequations by fixpoint iteration.
  • Parmov: compilation of parallel assignments. +
  • UnionFind: a persistent union-find data structure. -

    Definitions and properties used in many parts of the development

    +

    Definitions and theorems used in many parts of the development

    @@ -151,7 +153,9 @@ code. Cshmgenproof2
    Cshmgenproof3 - Stack allocation of local variables
    whose address is taken + Stack allocation of local variables
    + whose address is taken;
    + simplification of switch statements Csharpminor to Cminor Cminorgen Cminorgenproof @@ -160,8 +164,10 @@ code. Recognition of operators
    and addressing modes Cminor to CminorSel - Selection - Selectionproof + Selection
    + SelectOp + Selectionproof
    + SelectOpproof @@ -182,8 +188,10 @@ code. Constant propagation RTL to RTL - Constprop - Constpropproof + Constprop
    + ConstpropOp + Constpropproof
    + ConstproppOproof @@ -276,7 +284,7 @@ Proofs that compiler passes are type-preserving:

    All together

    -- cgit v1.2.3