From a78ec9a93ab9c1c3ab240d8f86332e3dad773b27 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 18 Aug 2017 11:50:38 +0200 Subject: Update documentation index for release 3.1 --- doc/index.html | 40 +++++++++++++++++----------------------- 1 file changed, 17 insertions(+), 23 deletions(-) diff --git a/doc/index.html b/doc/index.html index 239bdb28..d2a5b6cc 100644 --- a/doc/index.html +++ b/doc/index.html @@ -24,11 +24,11 @@ a:active {color : Red; text-decoration : underline; }

The CompCert verified compiler

Commented Coq development

-

Version 3.0, 2017-02-10

+

Version 3.1, 2017-08-18

Introduction

-

CompCert is a compiler that generates PowerPC, ARM and x86 assembly +

CompCert is a compiler that generates PowerPC, ARM, RISC-V and x86 assembly code from CompCert C, a large subset of the C programming language. The particularity of this compiler is that it is written mostly within the specification language of the Coq proof assistant, and its @@ -40,18 +40,14 @@ within the Coq proof assistant.

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 specifications and proofs. Proof scripts are folded by default, but -can be viewed by clicking on "Proof". Some modules (written in italics below) differ between the three supported target architectures. The -PowerPC versions of these modules are shown below; the ARM and x86 +can be viewed by clicking on "Proof". Some modules (written in italics below) differ between the four target architectures. The +PowerPC versions of these modules are shown below; the ARM, x86 and RISC-V versions can be found in the source distribution.

@@ -62,8 +58,7 @@ written.

The complete sources for CompCert can be downloaded from the CompCert Web site.

-

This document and the CompCert sources are -copyright 2005-2016 Institut +

This document and the CompCert sources are copyright Institut National de Recherche en Informatique et en Automatique (INRIA) and distributed under the terms of the following license. @@ -98,8 +93,7 @@ common elements of abstract syntaxes.

  • Linking: generic framework to define syntactic linking over the CompCert languages.
  • Values: run-time values.
  • Events: observable events and traces. -
  • Memtype: memory model (interface).
    -See also: Memory (implementation of the memory model).
    +
  • Memory: memory model.
    See also: Memdata (in-memory representation of data).
  • Globalenvs: global execution environments.
  • Smallstep: tools for small-step semantics. @@ -119,8 +113,8 @@ semantics. determinized semantics and type system.
    See also: type expressions and -operators (syntax and semantics) and -reference interpreter. +operators (syntax and semantics).
    +See also: reference interpreter.
  • Clight: a simpler version of CompCert C where expressions contain no side-effects.
  • Csharpminor: low-level structured language. @@ -317,6 +311,14 @@ code. +

    All together

    + + +

    Static analyses

    The following static analyses are performed over the RTL intermediate @@ -334,7 +336,7 @@ See also: NeedOp: processor-dependent part

    Type systems

    -The type system of CompCert C is fully formalized. For some intermediate languages of the back-end, simpler type systems are used to statically capture well-formedness conditions. +The type system of CompCert C is fully formalized. For some intermediate languages of the back-end, simpler type systems are used to statically capture well-formedness conditions. -

    All together

    - - -
    Xavier.Leroy@inria.fr
    -- cgit