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