diff options
-rw-r--r-- | Changelog | 18 | ||||
-rw-r--r-- | LICENSE | 4 | ||||
-rw-r--r-- | cparser/Elab.ml | 2 | ||||
-rw-r--r-- | doc/coq2html.css | 5 | ||||
-rw-r--r-- | doc/coq2html.mll | 32 | ||||
-rw-r--r-- | doc/index.html | 21 |
6 files changed, 61 insertions, 21 deletions
@@ -1,4 +1,4 @@ -Release 2.5, 2015-06-xx +Release 2.5, 2015-06-12 ======================= Language features: @@ -38,20 +38,21 @@ Usability: - Revised handling of arguments to __builtin_annot so that no code is generated for an argument that is a global variable or a local variable whose address is taken. -- In string and character literals, treat illegal escape sequences +- In string and character literals, treat illegal escape sequences (e.g. "\%" or "\0") as an error instead of a warning. - Warn if floating-point literals overflow or underflow when converted to FP numbers. -- cchecklink: added option "-files-from" to read .sdump file names - from a file or from standard input. -- In "-g -S" mode, annotate the generated .s file with comments +- In "-g -S" mode, annotate the generated .s file with comments containing the C source code. - Recognize and accept more of GCC's alternate keywords, e.g. __signed, __volatile__, etc. +- cchecklink: added option "-files-from" to read .sdump file names + from a file or from standard input. ABI conformance: - Improved ABI conformance for passing values of struct or union types - as function arguments or results. + as function arguments or results. Full conformance is achieved on + IA32/ELF, IA32/MacOSX, PowerPC/EABI, PowerPC/Linux, and ARM/EABI. - Support the "va_arg" macro from <stdarg.h> in the case of arguments of struct or union types. @@ -77,6 +78,11 @@ Bug fixing: - Issue #44: OSX assembler does not recognize ".global" directive. - Protect against redefinition of the __i64_xxx helper library functions. - Revised handling of nonstandard attributes in C type compatibility check. +- Emit an error on "preprocessing numbers" that are invalid numerical literals. +- Added missing check for static redefinition following a non-static + declaration. +- Added missing check for redefinition of a typedef as an ordinary + identifier within the same scope. Miscellaneous: - When preprocessing with gcc or clang, use "-std=c99" mode to force @@ -1,8 +1,8 @@ All files in this distribution are part of the CompCert verified compiler. The CompCert verified compiler is Copyright 2004, 2005, 2006, 2007, -2008, 2009, 2010, 2011, 2012, 2013, 2014 Institut National de Recherche en -Informatique et en Automatique (INRIA). +2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015 Institut National de +Recherche en Informatique et en Automatique (INRIA). The CompCert verified compiler is distributed under the terms of the INRIA Non-Commercial License Agreement given below. This is a diff --git a/cparser/Elab.ml b/cparser/Elab.ml index bcf90f5e..aa015b83 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -640,7 +640,7 @@ and elab_field_group env (Field_group (spec, fieldlist, loc)) = error loc "non-default storage in struct or union"; if fieldlist = [] then if is_anonymous_composite spec then - error loc "ISO C99 does not support anonymous structs/unions" + warning loc "ISO C99 does not support anonymous structs/unions" else warning loc "declaration does not declare any members"; diff --git a/doc/coq2html.css b/doc/coq2html.css index 0f6680e8..c5627bfb 100644 --- a/doc/coq2html.css +++ b/doc/coq2html.css @@ -7,6 +7,7 @@ div.proofscript contents of proof script span.docright contents of (**r *) comments span.bracket contents of [ ] within comments + span.comment contents of (* *) comments span.kwd Coq keyword span.tactic Coq tactic span.id any other identifier @@ -86,6 +87,10 @@ span.kwd { color: #cf1d1d; } +span.comment { + color: #008000; +} + a:visited {color : #416DFF; text-decoration : none; } a:link {color : #416DFF; text-decoration : none; } a:hover {text-decoration : none; } diff --git a/doc/coq2html.mll b/doc/coq2html.mll index 329e9eaa..2f1bfdbc 100644 --- a/doc/coq2html.mll +++ b/doc/coq2html.mll @@ -206,15 +206,23 @@ let start_verbatim () = let end_verbatim () = fprintf !oc "</pre>\n" +let start_comment () = + fprintf !oc "<span class=\"comment\">(*" + +let end_comment () = + fprintf !oc "*)</span>" + let start_bracket () = fprintf !oc "<span class=\"bracket\">" let end_bracket () = fprintf !oc "</span>" +let in_proof = ref false let proof_counter = ref 0 let start_proof kwd = + in_proof := true; incr proof_counter; fprintf !oc "<div class=\"toggleproof\" onclick=\"toggleDisplay('proof%d')\">%s</div>\n" @@ -222,7 +230,8 @@ let start_proof kwd = fprintf !oc "<div class=\"proofscript\" id=\"proof%d\">\n" !proof_counter let end_proof kwd = - fprintf !oc "%s</div>\n" kwd + fprintf !oc "%s</div>\n" kwd; + in_proof := false let start_html_page modname = fprintf !oc "\ @@ -300,7 +309,8 @@ and coq = parse end_doc_right(); coq lexbuf } | "(*" - { comment lexbuf; + { if !in_proof then start_comment(); + comment lexbuf; coq lexbuf } | path as id { ident (Lexing.lexeme_start lexbuf) id; coq lexbuf } @@ -325,13 +335,23 @@ and bracket = parse and comment = parse | "*)" - { () } + { if !in_proof then end_comment() } | "(*" - { comment lexbuf; comment lexbuf } + { if !in_proof then start_comment(); + comment lexbuf; comment lexbuf } | eof { () } - | _ - { comment lexbuf } + | "\n" + { if !in_proof then newline(); + comment lexbuf } + | space* as s + { if !in_proof then space s; + comment lexbuf } + | eof + { () } + | _ as c + { if !in_proof then character c; + comment lexbuf } and doc_bol = parse | "<<" space* "\n" diff --git a/doc/index.html b/doc/index.html index 296d89e0..29a2fb30 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 2.3, 2015-05-05</H3> +<H3 align="center">Version 2.5, 2015-06-12</H3> <H2>Introduction</H2> @@ -63,7 +63,8 @@ written.</P> <A HREF="http://compcert.inria.fr/">the CompCert Web site</A>.</P> <P>This document and the CompCert sources are -copyright 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014 Institut +copyright 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015 +Institut National de Recherche en Informatique et en Automatique (INRIA) and distributed under the terms of the following <A HREF="LICENSE">license</A>. @@ -115,7 +116,8 @@ semantics. <LI> The CompCert C source language: <A HREF="html/Csyntax.html">syntax</A> and <A HREF="html/Csem.html">semantics</A> and -<A HREF="html/Cstrategy.html">determinized semantics</A>.<BR> +<A HREF="html/Cstrategy.html">determinized semantics</A> and +<A HREF="html/Ctyping.html">type system</A>.<BR> See also: <A HREF="html/Ctypes.html">type expressions</A> and <A HREF="html/Cop.html">operators (syntax and semantics)</A> and <A HREF="html/Cexec.html">reference interpreter</A>. @@ -245,13 +247,20 @@ code. </TR> <TR valign="top"> - <TD>Dead code elimination</TD> + <TD>Redundancy elimination</TD> <TD>RTL to RTL</TD> <TD><A HREF="html/Deadcode.html">Deadcode</A></TD> <TD><A HREF="html/Deadcodeproof.html">Deadcodeproof</A></TD> </TR> <TR valign="top"> + <TD>Removal of unused static globals</TD> + <TD>RTL to RTL</TD> + <TD><A HREF="html/Unusedglob.html">Unusedglob</A></TD> + <TD><A HREF="html/Unusedglobproof.html">Unusedglobproof</A></TD> +</TR> + +<TR valign="top"> <TD>Register allocation (validation a posteriori)</TD> <TD>RTL to LTL</TD> <TD><A HREF="html/Allocation.html">Allocation</A></TD> @@ -315,9 +324,9 @@ See also: <A HREF="html/NeedOp.html"><I>NeedOp</I></A>: processor-dependent part <H3>Type systems</H3> -Simple type systems are used to statically capture well-formedness -conditions on some intermediate languages. +The type system of CompCert C is fully formalized. For some intermediate languages of the back-end, simpler type systems are used to statically capture well-formedness conditions. <UL> +<LI> <A HREF="html/Ctyping.html">RTLtyping</A>: typing for CompCert C + type-checking functions. <LI> <A HREF="html/RTLtyping.html">RTLtyping</A>: typing for RTL + type reconstruction. <LI> <A HREF="html/Lineartyping.html">Lineartyping</A>: typing for Linear. |