From fd6bc3111af1e115fd9c8d653056393fe40715ca Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 21 Sep 2010 08:10:53 +0000 Subject: Update for release 1.8 git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1512 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- Changelog | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) (limited to 'Changelog') diff --git a/Changelog b/Changelog index 2842d3b..cc154e2 100644 --- a/Changelog +++ b/Changelog @@ -1,15 +1,16 @@ -Release 1.8 -=========== +Release 1.8, 2010-09-21 +======================= - The input language to the proved part of the compiler is no longer Clight but CompCert C: a larger subset of the C language supporting - in particular side-effects within expressions. The transformation - that pulls side effects out of expressions, formerly performed by - untrusted Caml code, is now fully proved in Coq. + in particular side-effects within expressions. The transformations + that pull side effects out of expressions and materialize implicit + casts, formerly performed by untrusted Caml code, are now fully + proved in Coq. - New port targeting Intel/AMD x86 processors. Generates 32-bit x86 code using SSE2 extensions for floating-point arithmetic. Works under - Linux, *BSD, MacOS X, and the Cygwin environment for Windows. + Linux, MacOS X, and the Cygwin environment for Windows. CompCert's compilation strategy is not a very good match for the x86 architecture, therefore the performance of the generated code is not as good as for the PowerPC port, but still usable. -- cgit v1.2.3