diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-09-21 08:10:53 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-09-21 08:10:53 +0000 |
| commit | fd6bc3111af1e115fd9c8d653056393fe40715ca (patch) | |
| tree | 369a58c80898a7cdb64da7c7f9e7d1c36a9ccd45 /Changelog | |
| parent | 771e05d46a08d412ea05adf7b147e0291215b92b (diff) | |
Update for release 1.8
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1512 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'Changelog')
| -rw-r--r-- | Changelog | 13 |
1 files changed, 7 insertions, 6 deletions
@@ -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. |