summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Changelog4
-rw-r--r--LICENSE6
-rw-r--r--README2
-rw-r--r--doc/coq2html.mll2
-rw-r--r--doc/index.html31
5 files changed, 34 insertions, 11 deletions
diff --git a/Changelog b/Changelog
index 8984ee8..f5bfbbf 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 3b41c10..567ef04 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 501b439..e949297 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 4f04f98..329e9ea 100644
--- a/doc/coq2html.mll
+++ b/doc/coq2html.mll
@@ -230,7 +230,7 @@ let start_html_page modname =
<html xmlns=\"http://www.w3.org/1999/xhtml\">
<head>
-<meta http-equiv=\"Content-Type\" content=\"text/html; charset=iso-8859-1\" />
+<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\" />
<title>Module %s</title>
<meta name=\"description\" content=\"Documentation of Coq module %s\" />
<link href=\"coq2html.css\" rel=\"stylesheet\" type=\"text/css\" />
diff --git a/doc/index.html b/doc/index.html
index 36989ff..1845851 100644
--- a/doc/index.html
+++ b/doc/index.html
@@ -24,7 +24,7 @@ a:active {color : Red; text-decoration : underline; }
<H1 align="center">The CompCert verified compiler</H1>
<H2 align="center">Commented Coq development</H2>
-<H3 align="center">Version 2.1, 2013-10-28</H3>
+<H3 align="center">Version 2.2, 2014-02-24</H3>
<H2>Introduction</H2>
@@ -63,7 +63,7 @@ written.</P>
<A HREF="http://compcert.inria.fr/">the CompCert Web site</A>.</P>
<P>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 <A HREF="LICENSE">license</A>.
@@ -188,9 +188,11 @@ code.
<TD>Cminor to CminorSel</TD>
<TD><A HREF="html/Selection.html">Selection</A><br>
<A HREF="html/SelectOp.html"><I>SelectOp</I></A><br>
+ <A HREF="html/SelectDiv.html">SelectDiv</A><br>
<A HREF="html/SelectLong.html">SelectLong</A></TD>
<TD><A HREF="html/Selectionproof.html">Selectionproof</A><br>
<A HREF="html/SelectOpproof.html"><I>SelectOpproof</I></A><br>
+ <A HREF="html/SelectDiv.html">SelectDiv</A><br>
<A HREF="html/SelectLongproof.html">SelectLongproof</A></TD>
</TR>
@@ -228,8 +230,7 @@ code.
<TD>Constant propagation</TD>
<TD>RTL to RTL</TD>
<TD><A HREF="html/Constprop.html">Constprop</A><br>
- <A HREF="html/ConstpropOp.html"><I>ConstpropOp</I></A><br>
- <A HREF="html/Liveness.html">Liveness</A></TD>
+ <A HREF="html/ConstpropOp.html"><I>ConstpropOp</I></A></TD>
<TD><A HREF="html/Constpropproof.html">Constpropproof</A><br>
<A HREF="html/ConstpropOpproof.html"><I>ConstproppOproof</I></A></TD>
</TR>
@@ -244,6 +245,13 @@ code.
</TR>
<TR valign="top">
+ <TD>Dead code elimination</TD>
+ <TD>RTL to RTL</TD>
+ <TD><A HREF="html/Deadcode.html">Deadcode</A></TD>
+ <TD><A HREF="html/Deadcodeproof.html">Deadcodeproof</A></TD>
+</TR>
+
+<TR valign="top">
<TD>Register allocation (validation a posteriori)</TD>
<TD>RTL to LTL</TD>
<TD><A HREF="html/Allocation.html">Allocation</A></TD>
@@ -290,6 +298,21 @@ code.
</TR>
</TABLE>
+<H3>Static analyses</H3>
+
+The following static analyses are performed over the RTL intermediate
+representation to support optimizations such as constant propagation,
+CSE, and dead code elimination.
+<UL>
+<LI> <A HREF="html/Liveness.html">Liveness</A>: liveness analysis</A>.
+<LI> <A HREF="html/ValueAnalysis.html">ValueAnalysis</A>: value and alias analysis</A> <BR>
+See also: <A HREF="html/ValueDomain.html">ValueDomain</A>: the abstract domain for value analysis.<BR>
+See also: <A HREF="html/ValueAOp.html"><I>ValueAOp</I></A>: processor-dependent parts of value analysis.
+<LI> <A HREF="html/Deadcode.html">Deadcode</A>: neededness analysis</A> <BR>
+See also: <A HREF="html/NeedDomain.html">NeedDomain</A>: the abstract domain for neededness analysis.<BR>
+See also: <A HREF="html/NeedOp.html"><I>NeedOp</I></A>: processor-dependent parts of neededness analysis.
+</UL>
+
<H3>Type systems</H3>
Trivial type systems are used to statically capture well-formedness