From a3d4f94f470f1ad1b9406c67589c9ebc44c94113 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 11 Jun 2015 16:18:46 +0200 Subject: Update for release 2.5. --- doc/index.html | 21 +++++++++++++++------ 1 file changed, 15 insertions(+), 6 deletions(-) (limited to 'doc') diff --git a/doc/index.html b/doc/index.html index 296d89e0..29a2fb30 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 2.3, 2015-05-05

+

Version 2.5, 2015-06-12

Introduction

@@ -63,7 +63,8 @@ written.

the CompCert Web site.

This document and the CompCert sources are -copyright 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014 Institut +copyright 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015 +Institut National de Recherche en Informatique et en Automatique (INRIA) and distributed under the terms of the following license. @@ -115,7 +116,8 @@ semantics.

  • The CompCert C source language: syntax and semantics and -determinized semantics.
    +determinized semantics and +type system.
    See also: type expressions and operators (syntax and semantics) and reference interpreter. @@ -245,12 +247,19 @@ code. - Dead code elimination + Redundancy elimination RTL to RTL Deadcode Deadcodeproof + + Removal of unused static globals + RTL to RTL + Unusedglob + Unusedglobproof + + Register allocation (validation a posteriori) RTL to LTL @@ -315,9 +324,9 @@ See also: NeedOp: processor-dependent part

    Type systems

    -Simple type systems are used to statically capture well-formedness -conditions on some intermediate languages. +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.