From 6c22a0fe2545bf65acdbd067aea25f6e1b96a7cd Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 15 Jul 2009 12:04:30 +0000 Subject: MAJ git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1107 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- doc/index.html | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) (limited to 'doc') diff --git a/doc/index.html b/doc/index.html index a5741f5..47c849e 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.3, 2008-08-11

+

Version 1.4, 2009-04-21

Introduction

@@ -36,10 +36,10 @@ correctness --- the fact that the generated assembly code is semantically equivalent to its source program --- was entirely proved within the Coq proof assistant.

-

A high-level overview of the Compcert compiler and its proof of -correctness can be found in the following papers:

+

High-level descriptions of the Compcert compiler and its proof of +correctness can be found in the following papers (in increasing order of technical details):

This Web site gives a commented listing of the underlying Coq @@ -127,7 +128,7 @@ spilling, reloading and enforcement of calling conventions. view of the activation record.
See also: Machabstr abstract semantics for Mach.
See also: Machconcr concrete semantics for Mach. -

  • PPC: abstract syntax for PowerPC assembly +
  • Asm: abstract syntax for PowerPC assembly code. @@ -238,15 +239,15 @@ code. Storing the activation records in memory Mach to Mach (none) - PPCgenretaddr
    + Asmgenretaddr
    Machabstr2concr - Emission of PowerPC assembly - Mach to PPC - PPCgen - PPCgenproof1
    - PPCgenproof + Emission of assembly code + Mach to Asm + Asmgen + Asmgenproof1
    + Asmgenproof -- cgit v1.2.3