From 9b31f673da13a4f4d04d937ac2b9e934c9b8291d Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 22 Jun 2016 11:18:21 +0200 Subject: Update in preparation for release 2.7 --- Changelog | 46 ++++++++++++++++++++++++++++++++++++++++++++++ doc/index.html | 6 +++--- 2 files changed, 49 insertions(+), 3 deletions(-) diff --git a/Changelog b/Changelog index 9ce8703c..7d53cb5c 100644 --- a/Changelog +++ b/Changelog @@ -1,3 +1,49 @@ +Release 2.7, 2016-06-29 +======================= + +Major improvement: +- The proof of semantic preservation now accounts for separate compilation + and linking, following the approach of Kang, Kim, Hur, Dreyer and + Vafeiadis, "Lightweight verification of separate compilation", POPL 2016. + Namely, the proof considers a set of C compilation units, separately + compiled to assembly then linked, and shows that the resulting + assembly program preserves the semantics of the C program that would + be obtained by syntactic linking of the source C compilation units. + +Language features: +- Parse the _Noreturn function attribute from ISO C11. +- New standard includes files: and from ISO C11. +- New built-in functions: __builtin_clzl, __builtin_clzll + (count leading zeros, 32 and 64 bits) for ARM, IA32 and PowerPC; + __builtin_ctz, __builtin_ctzl, __builtin_ctzll + (count trailing zeros, 32 and 64 bits) for IA32. + +Formal C semantics: +- The semantics of conversions from pointer types to _Bool + is fully defined (again). + +Coq development: +- Revised the Stacking pass and its proof to make it more extensible + later to e.g. 64-bit integer registers. +- Use register pairs in function calling conventions to control more + precisely the splitting of 64-bit integer arguments and results + into pairs of 32-bit quantities +- Revised the way register conventions are described in Machregs + and Conventions. +- Simulation diagrams now live in Prop instead of Type. + +OCaml development: +- Code cleanup to remove warnings, support "safe strings" mode, + and be fully compatible with OCaml 4.02 and 4.03. +- Cminor parser: support for single-precision FP numbers and operators. + +Bug fixing: +- Some declarations within C expressions were incorrectly ignored + (e.g. "sizeof(enum e {A})"). +- ARM in Thumb mode: incorrect "movs" instructions involving the stack + pointer register were generated. + + Release 2.6, 2015-12-21 ======================= diff --git a/doc/index.html b/doc/index.html index ae6e8382..023267d0 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.6, 2015-12-21

+

Version 2.7, 2016-06-29

Introduction

@@ -63,8 +63,7 @@ written.

the CompCert Web site.

This document and the CompCert sources are -copyright 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015 -Institut +copyright 2005-2016 Institut National de Recherche en Informatique et en Automatique (INRIA) and distributed under the terms of the following license. @@ -96,6 +95,7 @@ inequations by fixpoint iteration.

  • Errors: the Error monad.
  • AST: identifiers, whole programs and other common elements of abstract syntaxes. +
  • Linking: generic framework to define syntactic linking over the CompCert languages.
  • Values: run-time values.
  • Events: observable events and traces.
  • Memtype: memory model (interface).
    -- cgit