diff options
-rw-r--r-- | Changelog | 31 | ||||
-rw-r--r-- | README | 4 |
2 files changed, 33 insertions, 2 deletions
@@ -1,3 +1,34 @@ +Release 1.5 +========= + +- Support for "goto" in the source language Clight. + +- Added small-step semantics for Clight. + +- Traces for diverging executions are now uniquely defined; + tightened semantic preservation results accordingly. + +- Fixed spurious compile-time error on Clight statements of the form + "x = f(...)" where x is a global variable. + +- Fixed spurious compile-time error on Clight initializers where + the initial value is the result of a floating-point computation + (e.g. "double x = 3.14159 / 2;"). + +- Simplified the interface of the generic dataflow solver. + +- Reduced running time and memory requirements for the constant propagation + pass. + +- Improved the implementation of George and Appel's graph coloring heuristic: + runs faster, produces better results. + +- Revised the implementation of branch tunneling. + +- Improved modularization between processor-dependent and + processor-independent parts. + + Release 1.4.1, 2009-06-05 ========================= @@ -46,7 +46,7 @@ PREREQUISITES: the search path. For MacOS X, you can get them by installing the XCode development tools, as found on the installation DVDs. -* The Coq proof assistant, version 8.1pl3. +* The Coq proof assistant, version 8.2-1 or later. Coq is free software, available from http://coq.inria.fr/ * The Caml functional language, version 3.10 or later. @@ -121,7 +121,7 @@ The generated assembly code is left in file src1.s The subset of the C language accepted by Compcert is quite large. The main features of C that are not supported are: - The "long long" and "long double" types. - - The "goto" statement, and non-structured forms of the "switch" statement. + - Non-structured forms of the "switch" statement (Duff's device). - Variable-argument functions. The "ccomp" command will issue errors and diagnostics if it encounters a C construct that it cannot process. |