diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-07-30 15:35:29 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-07-30 15:35:29 +0000 |
commit | 603e931f49ef04188a58895ce38d892511b75b78 (patch) | |
tree | 41f1f2fe83718bf241421c5f185a696d0fab6c7a /Changelog | |
parent | 1fe68ad575178f7d8a775906947d2fed94d40976 (diff) |
ARM: added reversed load/store builtins + bswap builtin (to be tested)
IA32: added bswap builtin
Updated Changelog
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1693 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'Changelog')
-rw-r--r-- | Changelog | 27 |
1 files changed, 23 insertions, 4 deletions
@@ -1,7 +1,14 @@ -- Fixed two omissions in the semantics of CompCert C (reported by Brian Campbell): - . Functions calls through a function pointer had undefined semantics. - . Conditional expressions "e1 ? e2 : e3" where e2 and e3 have different - types were missing a cast to their common type. +Release 1.9, 2011-xx-xx +======================= + +- The reduction semantics of CompCert C was made executable and turned + into a reference interpreter for CompCert C, enabling animation of + the semantics. (Thanks to Brian Campbell for suggesting this approach.) + Usage is: ccomp -interp [options] source.c + Options include: + -trace to print a detailed trace of reduction steps + -random to randomize execution order + -all to explore all possible execution orders in parallel - Revised and strengthened the top-level statements of semantic preservation. In particular, we now show: @@ -11,6 +18,11 @@ the compiled code performs at least these I/O before continuing with an arbitrary behavior. +- Fixed two omissions in the semantics of CompCert C (reported by Brian Campbell): + . Functions calls through a function pointer had undefined semantics. + . Conditional expressions "e1 ? e2 : e3" where e2 and e3 have different + types were missing a cast to their common type. + - Revised handling of annotation statements. Now they come in two forms: 1. __builtin_annot("format", x1, ..., xN) (arbitrarily many arguments; no code generated, even if some @@ -22,6 +34,13 @@ - Related clean-ups in the handling of external functions and compiler built-ins. +- ARM code generator was ported to the new ABI (EABI in ARM parlance, + armel in Debian parlance), using VFD instructions for floating-point. + (Successfully tested on a Trimslice platform running Ubuntu 11.04.) + +- IA32 code generator: added -fno-sse option to prevent generation of + SSE instructions for memory copy operations. + Release 1.8.2, 2011-05-24 ========================= |