From fd6bc3111af1e115fd9c8d653056393fe40715ca Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 21 Sep 2010 08:10:53 +0000 Subject: Update for release 1.8 git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1512 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- doc/index.html | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) (limited to 'doc/index.html') diff --git a/doc/index.html b/doc/index.html index 07ab0ff3..67b821f0 100644 --- a/doc/index.html +++ b/doc/index.html @@ -24,12 +24,12 @@ a:active {color : Red; text-decoration : underline; }

The Compcert verified compiler

Commented Coq development

-

Version 1.7, 2010-03-31

+

Version 1.8, 2010-09-21

Introduction

-

Compcert is a compiler that generates PowerPC and ARM assembly -code from Clight, a large subset of the C programming language. +

Compcert is a compiler that generates PowerPC, ARM 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 correctness --- the fact that the generated assembly code is @@ -104,7 +104,7 @@ semantics.

Source, intermediate and target languages: syntax and semantics