Merge branch 'master' into asmexpand

Changelog

-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

LICENSE

 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

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";
 

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; }

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"

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,12 +247,19 @@ 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>
@@ -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.