diff options
| -rw-r--r-- | Changelog | 6 | ||||
| -rw-r--r-- | cfrontend/Csem.v | 18 | ||||
| -rw-r--r-- | doc/index.html | 24 |
3 files changed, 28 insertions, 20 deletions
@@ -1,5 +1,5 @@ -Release 1.5 -========= +Release 1.5, 2009-08-28 +======================= - Support for "goto" in the source language Clight. @@ -9,7 +9,7 @@ Release 1.5 tightened semantic preservation results accordingly. - Fixed spurious compile-time error on Clight statements of the form - "x = f(...)" where x is a global variable. + "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 diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index e0d05f2..ee13487 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -628,20 +628,20 @@ End EXPR. Inductive cont: Type := | Kstop: cont | Kseq: statement -> cont -> cont - (* [Kseq s2 k] = after [s1] in [s1;s2] *) + (**r [Kseq s2 k] = after [s1] in [s1;s2] *) | Kwhile: expr -> statement -> cont -> cont - (* [Kwhile e s k] = after [s] in [while (e) s] *) + (**r [Kwhile e s k] = after [s] in [while (e) s] *) | Kdowhile: expr -> statement -> cont -> cont - (* [Kdowhile e s k] = after [s] in [do s while (e)] *) + (**r [Kdowhile e s k] = after [s] in [do s while (e)] *) | Kfor2: expr -> statement -> statement -> cont -> cont - (* [Kfor2 e2 e3 s k] = after [s] in [for(e1;e2;e3) s] *) + (**r [Kfor2 e2 e3 s k] = after [s] in [for(e1;e2;e3) s] *) | Kfor3: expr -> statement -> statement -> cont -> cont - (* [Kfor3 e2 e3 s k] = after [e3] in [for(e1;e2;e3) s] *) + (**r [Kfor3 e2 e3 s k] = after [e3] in [for(e1;e2;e3) s] *) | Kswitch: cont -> cont - (* catches [break] statements arising out of [switch] *) - | Kcall: option (block * int * type) -> (* where to store result *) - function -> (* calling function *) - env -> (* local env of calling function *) + (**r catches [break] statements arising out of [switch] *) + | Kcall: option (block * int * type) -> (**r where to store result *) + function -> (**r calling function *) + env -> (**r local env of calling function *) cont -> cont. (** Pop continuation until a call or stop *) diff --git a/doc/index.html b/doc/index.html index 47c849e..88151d1 100644 --- a/doc/index.html +++ b/doc/index.html @@ -24,7 +24,7 @@ a:active {color : Red; text-decoration : underline; } <H1 align="center">The Compcert verified compiler</H1> <H2 align="center">Commented Coq development</H2> -<H3 align="center">Version 1.4, 2009-04-21</H3> +<H3 align="center">Version 1.5, 2009-08-28</H3> <H2>Introduction</H2> @@ -83,9 +83,10 @@ semi-lattices. <LI> <A HREF="html/Kildall.html">Kildall</A>: resolution of dataflow inequations by fixpoint iteration. <LI> <A HREF="html/Parmov.html">Parmov</A>: compilation of parallel assignments. +<LI> <A HREF="html/UnionFind.html">UnionFind</A>: a persistent union-find data structure. </UL> -<H3>Definitions and properties used in many parts of the development</H3> +<H3>Definitions and theorems used in many parts of the development</H3> <UL> <LI> <A HREF="html/Errors.html">Errors</A>: the Error monad. @@ -96,6 +97,7 @@ common elements of abstract syntaxes. <LI> <A HREF="html/Mem.html">Mem</A>: the memory model. <LI> <A HREF="html/Globalenvs.html">Globalenvs</A>: global execution environments. <LI> <A HREF="html/Smallstep.html">Smallstep</A>: tools for small-step semantics. +<LI> <A HREF="html/Determinism.html">Determinism</A>: determinism properties of small-step semantics. <LI> <A HREF="html/Op.html">Op</A>: operators, addressing modes and their semantics. </UL> @@ -151,7 +153,9 @@ code. <A HREF="html/Cshmgenproof2.html">Cshmgenproof2</A><br> <A HREF="html/Cshmgenproof3.html">Cshmgenproof3</A></TD> <TR valign="top"> - <TD>Stack allocation of local variables<br>whose address is taken</TD> + <TD>Stack allocation of local variables<br> + whose address is taken;<br> + simplification of switch statements</TD> <TD>Csharpminor to Cminor</TD> <TD><A HREF="html/Cminorgen.html">Cminorgen</A></TD> <TD><A HREF="html/Cminorgenproof.html">Cminorgenproof</A></TD> @@ -160,8 +164,10 @@ code. <TR valign="top"> <TD>Recognition of operators<br>and addressing modes</TD> <TD>Cminor to CminorSel</TD> - <TD><A HREF="html/Selection.html">Selection</A></TD> - <TD><A HREF="html/Selectionproof.html">Selectionproof</A></TD> + <TD><A HREF="html/Selection.html">Selection</A><br> + <A HREF="html/SelectOp.html">SelectOp</A></TD> + <TD><A HREF="html/Selectionproof.html">Selectionproof</A><br> + <A HREF="html/SelectOpproof.html">SelectOpproof</A></TD> </TR> <TR valign="top"> @@ -182,8 +188,10 @@ code. <TR valign="top"> <TD>Constant propagation</TD> <TD>RTL to RTL</TD> - <TD><A HREF="html/Constprop.html">Constprop</A></TD> - <TD><A HREF="html/Constpropproof.html">Constpropproof</A></TD> + <TD><A HREF="html/Constprop.html">Constprop</A><br> + <A HREF="html/ConstpropOp.html">ConstpropOp</A></TD> + <TD><A HREF="html/Constpropproof.html">Constpropproof</A><br> + <A HREF="html/ConstpropOpproof.html">ConstproppOproof</A></TD> </TR> <TR valign="top"> @@ -276,7 +284,7 @@ Proofs that compiler passes are type-preserving: <H3>All together</H3> <UL> -<LI> <A HREF="html/Main.html">Main</A>: composing the passes together; the +<LI> <A HREF="html/Compiler.html">Compiler</A>: composing the passes together; the final semantic preservation theorems. <LI> <A HREF="html/Complements.html">Complements</A>: interesting consequences of the semantic preservation theorems. </UL> |