From 93a33f710ed9a5eb045d8ee09b6142142b172f18 Mon Sep 17 00:00:00 2001
From: xleroy
Date: Wed, 9 Jan 2013 10:35:04 +0000
Subject: Update for release 1.12
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2097 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
Changelog | 15 +++++++++++++--
LICENSE | 8 +++++---
README | 2 +-
doc/index.html | 11 ++++++++---
4 files changed, 27 insertions(+), 9 deletions(-)
diff --git a/Changelog b/Changelog
index 23cbba83..89551a2b 100644
--- a/Changelog
+++ b/Changelog
@@ -1,4 +1,4 @@
-Release 1.12
+Release 1.12, 2013-01-11
========================
Improvements in confidence:
@@ -26,12 +26,22 @@ Performance improvements:
- More aggressive elimination of conditional branches during constant
propagation, taking better advantage of inferred constants.
-Internal simplifications:
+Language features:
+- By popular demand, "asm" statements for inline assembly are now supported
+ if the flag -finline-asm is set. Use with extreme caution, as the
+ semantic preservation proof assumes these statements have no effect
+ on the processor state.
+
+Internal simplifications and reorganization:
- Clight, Csharpminor, Cminor: suppressed the "Econdition" conditional
expressions, no longer useful.
- Clight: a single loop form, the three C loops are derived forms.
- Clight: volatile memory accesses are materialized as builtin operations.
- Clight: removed dependencies on CompCert C syntax and semantics.
+- New pass SimplLocals over Clight that replaces local scalar variables
+ whose address is never taken by temporary, nonadressable variables.
+ (This used to be done in Cminorgen.)
+- Csharpminor: simplified semantics.
- Cminor: suppressed the "Oboolval" and "Onotbool" operators,
which can be expressed in terms of "Ocmpu" at no performance costs.
- All languages: programs are now presented as a list of global definitions
@@ -42,6 +52,7 @@ Other changes:
- For compatibility with other C compilers, output files are now generated
in the current directory, by default; output file name can be controlled
with the -o option, somewhat like with GCC.
+- Reference interpreter: better handling of volatile memory accesses.
- IA32/MacOS X: now supports referencing global variables defined in shared
libraries; old hack for stdio is no longer needed.
- PowerPC/MacOS X: this port was removed, as recent version of MacOS X
diff --git a/LICENSE b/LICENSE
index a6155925..5fec6cbb 100644
--- a/LICENSE
+++ b/LICENSE
@@ -1,8 +1,8 @@
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 Institut National de Recherche en Informatique
-et en Automatique (INRIA).
+2008, 2009, 2010, 2011, 2012, 2013 Institut National de Recherche en
+Informatique et en Automatique (INRIA).
The CompCert verified compiler is distributed under the terms of the
INRIA Non-Commercial License Agreement given below. This is a
@@ -29,7 +29,9 @@ option) any later version:
cfrontend/Cstrategy.v lib/Maps.v
cfrontend/Clight.v lib/Parmov.v
cfrontend/PrintCsyntax.ml lib/Camlcoq.ml
- cfrontend/PrintClight.ml
+ cfrontend/PrintClight.ml
+ exportclight/Clightdefs.v
+ exportclight/ExportClight.ml
all files in the runtime/ directory
all files in the cparser/ directory
diff --git a/README b/README
index fa8d4358..501b439e 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 Institut National de Recherche en
+2008, 2009, 2010, 2011, 2012, 2013 Institut National de Recherche en
Informatique et en Automatique (INRIA). It is distributed under the
conditions stated in file LICENSE.
diff --git a/doc/index.html b/doc/index.html
index 095f0823..172e18e2 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 1.11, 2012-07-13
+Version 1.12, 2013-01-11
Introduction
@@ -63,7 +63,7 @@ written.
the Compcert Web site.
This document and the Compcert sources are
-copyright 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012 Institut
+copyright 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013 Institut
National de Recherche en Informatique et en Automatique (INRIA) and
distributed under the terms of the
following license.
@@ -120,7 +120,6 @@ See also: type expressions and
operators (syntax and semantics) and
reference interpreter.
Clight: a simpler version of CompCert C where expressions contain no side-effects.
-operators (syntax and semantics).
Csharpminor: low-level
structured language.
Cminor: low-level structured
@@ -165,6 +164,12 @@ code.
SimplExprspec
SimplExprproof |
+
+ Pulling non-adressable scalar local variables out of memory |
+ Clight to Clight |
+ SimplLocals |
+ SimplLocalsproof
+
Simplification of control structures;
explication of type-dependent computations |
--
cgit