From 5af448143e8d548a8d73d8ed613156e331ca0e0b Mon Sep 17 00:00:00 2001
From: xleroy
Date: Fri, 21 Feb 2014 13:05:16 +0000
Subject: Updates for release 2.2
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2415 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
Changelog | 4 ++--
LICENSE | 6 +++---
README | 2 +-
doc/coq2html.mll | 2 +-
doc/index.html | 31 +++++++++++++++++++++++++++----
5 files changed, 34 insertions(+), 11 deletions(-)
diff --git a/Changelog b/Changelog
index 8984ee8c..f5bfbbff 100644
--- a/Changelog
+++ b/Changelog
@@ -1,5 +1,5 @@
-Release 2.2
-===========
+Release 2.2, 2014-02-24
+=======================
Major improvements:
diff --git a/LICENSE b/LICENSE
index 3b41c108..567ef04e 100644
--- a/LICENSE
+++ b/LICENSE
@@ -1,7 +1,7 @@
All files in this distribution are part of the CompCert verified compiler.
The CompCert verified compiler is Copyright 2004, 2005, 2006, 2007,
-2008, 2009, 2010, 2011, 2012, 2013 Institut National de Recherche en
+2008, 2009, 2010, 2011, 2012, 2013, 2014 Institut National de Recherche en
Informatique et en Automatique (INRIA).
The CompCert verified compiler is distributed under the terms of the
@@ -60,13 +60,13 @@ Public License.
The files contained in the flocq/ directory and its subdirectories are
taken from the Flocq project, http://flocq.gforge.inria.fr/
-These files are Copyright 2010-2012 INRIA and distributed under the
+These files are Copyright 2010-2013 INRIA and distributed under the
terms of the GNU Lesser General Public Licence, either version 3 of
the licence, or (at your option) any later version. A copy of the GNU
Lesser General Public Licence version 3 is included below.
The files contained in the runtime/ directory and its subdirectories
-are Copyright 2013 INRIA and distributed under the terms of the BSD
+are Copyright 2013-2014 INRIA and distributed under the terms of the BSD
license, included below.
Finally, the following files are taken from the CIL library:
diff --git a/README b/README
index 501b439e..e9492973 100644
--- a/README
+++ b/README
@@ -23,7 +23,7 @@ refer to the user's manual: http://compcert.inria.fr/man/
COPYRIGHT:
The CompCert verified compiler is Copyright 2004, 2005, 2006, 2007,
-2008, 2009, 2010, 2011, 2012, 2013 Institut National de Recherche en
+2008, 2009, 2010, 2011, 2012, 2013, 2014 Institut National de Recherche en
Informatique et en Automatique (INRIA). It is distributed under the
conditions stated in file LICENSE.
diff --git a/doc/coq2html.mll b/doc/coq2html.mll
index 4f04f98d..329e9eaa 100644
--- a/doc/coq2html.mll
+++ b/doc/coq2html.mll
@@ -230,7 +230,7 @@ let start_html_page modname =
-
+
Module %s
diff --git a/doc/index.html b/doc/index.html
index 36989ffe..18458510 100644
--- a/doc/index.html
+++ b/doc/index.html
@@ -24,7 +24,7 @@ a:active {color : Red; text-decoration : underline; }
This document and the CompCert sources are
-copyright 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013 Institut
+copyright 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014 Institut
National de Recherche en Informatique et en Automatique (INRIA) and
distributed under the terms of the
following license.
@@ -188,9 +188,11 @@ code.
+
+The following static analyses are performed over the RTL intermediate
+representation to support optimizations such as constant propagation,
+CSE, and dead code elimination.
+
ValueAnalysis: value and alias analysis
+See also: ValueDomain: the abstract domain for value analysis.
+See also: ValueAOp: processor-dependent parts of value analysis.
+
Deadcode: neededness analysis
+See also: NeedDomain: the abstract domain for neededness analysis.
+See also: NeedOp: processor-dependent parts of neededness analysis.
+
+
Type systems
Trivial type systems are used to statically capture well-formedness
--
cgit