diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-06-19 07:38:24 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-06-19 07:38:24 +0000 |
commit | c3ff165355e49114364bd45cd7c145ccb248ca8f (patch) | |
tree | 384661b6b3e6538e9f31d692711cfef304cbd08a /Changelog | |
parent | 7babde436ca270ec16dd7aae9d0de2f9c8d08ca1 (diff) | |
download | compcert-c3ff165355e49114364bd45cd7c145ccb248ca8f.tar.gz compcert-c3ff165355e49114364bd45cd7c145ccb248ca8f.zip |
Updates in preparation for release 2.00
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2283 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'Changelog')
-rw-r--r-- | Changelog | 9 |
1 files changed, 4 insertions, 5 deletions
@@ -1,4 +1,4 @@ -Release 2.00, 2013-06-XX +Release 2.00, 2013-06-21 ======================== Major improvements: @@ -20,8 +20,7 @@ Major improvements: . two-address operations are treated more efficiently . no need to reserve processor registers for spilling and reloading. The improvements in quality of generated code is significant for - IA32 (because of its paucity of registers) and barely noticeable - for ARM and PowerPC. + IA32 (because of its paucity of registers) but less so for ARM and PowerPC. - Preliminary support for debugging information. The "-g" flag causes DWARF debugging information to be generated for line numbers @@ -49,7 +48,7 @@ Improvements in compiler usability: - Reduced memory requirements of constant propagation pass by forgetting compile-time approximations of dead variables. - More careful elaboration of C struct and union types into CompCert C - types, avoiding behaviors exponential in the nesting of structs. + types, avoiding behaviors exponential in the nesting of structs. Bug fixing: - Fixed parsing of labeled statements inside "switch" constructs, @@ -61,7 +60,7 @@ Bug fixing: Coq development: - Adapted the memory model to the needs of the VST project at Princeton: . Memory block identifiers are now of type "positive" instead of "Z" - . Strengthened preconditions in the definition of memory injections + . Strengthened invariants in the definition of memory injections and the specification of external calls. - The LTL intermediate language is now a CFG of basic blocks. - Suppressed the LTLin intermediate language, no longer used. |