From 617a3e0b1adf2869efa097829230da7166a7eefe Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 11 Mar 2013 09:32:03 +0000 Subject: Updating doc for 1.13 git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2142 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- doc/index.html | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) diff --git a/doc/index.html b/doc/index.html index aa1847f..1f5d3ed 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.12, 2013-01-11

+

Version 1.13, 2013-03-12

Introduction

@@ -140,8 +140,7 @@ replaced by a linear list of instructions with explicit branches and labels.
  • Linear: like LTLin, with explicit spilling, reloading and enforcement of calling conventions.
  • Mach: like Linear, with a more concrete -view of the activation record.
    -See also: Machsem operational semantics for Mach.
    +view of the activation record.
  • Asm: abstract syntax for PowerPC assembly code. @@ -298,15 +297,15 @@ code. Stacking
    Bounds
    Stacklayout - Stackingproof
    - Asmgenretaddr + Stackingproof Emission of assembly code Mach to Asm Asmgen - Asmgenproof1
    + Asmgenproof0
    + Asmgenproof1
    Asmgenproof @@ -321,7 +320,6 @@ reconstruction.
  • LTLtyping: typing for LTL.
  • LTLintyping: typing for LTLin.
  • Lineartyping: typing for Linear. -
  • Machtyping: typing for Mach. Proofs that compiler passes are type-preserving:

    All together

    -- cgit v1.2.3