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.
+- RTLtyping: typing for CompCert C + type-checking functions.
- RTLtyping: typing for RTL + type
reconstruction.
- Lineartyping: typing for Linear.
--
cgit