Merge branch 'master' of https://github.com/AbsInt/CompCert

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, 2015 Institut National de
-Recherche en Informatique et en Automatique (INRIA).
+The CompCert verified compiler is Copyright by Institut National de 
+Recherche en Informatique et en Automatique (INRIA) and
+AbsInt Angewandte Informatik GmbH.
 
 The CompCert verified compiler is distributed under the terms of the
-INRIA Non-Commercial License Agreement given below.  This is a
-non-free license that grants you the right to use the CompCert verified
-compiler for educational, research or evaluation purposes only, but
-prohibits commercial uses.
+INRIA Non-Commercial License Agreement given below or under the terms
+of a Software Usage Agreement of AbsInt Angewandte Informatik GmbH.
+The latter is a separate contract document.
+
+The INRIA Non-Commercial License Agreement is a non-free license that 
+grants you the right to use the CompCert verified compiler for 
+educational, research or evaluation purposes only, but prohibits 
+any commercial uses.
+
+For commercial use you need a Software Usage Agreement from 
+AbsInt Angewandte Informatik GmbH.
 
 The following files in this distribution are dual-licensed both under
 the INRIA Non-Commercial License Agreement and under the Free Software

cfrontend/C2C.ml

@@ -897,6 +897,28 @@ let rec groupSwitch = function
       let (fst, cases) = groupSwitch rem in
       (Cutil.sseq s.sloc s fst, cases)
 
+(* Test whether the statement contains case and give an *)
+let rec contains_case s = 
+  match s.sdesc with
+  | C.Sskip 
+  | C.Sdo _ 
+  | C.Sbreak
+  | C.Scontinue 
+  | C.Sswitch _ (* Stop at a switch *)
+  | C.Sgoto _ 
+  | C.Sreturn _ 
+  | C.Sdecl _ 
+  | C.Sasm _ ->  ()
+  | C.Sseq (s1,s2)
+  | C.Sif(_,s1,s2) -> contains_case s1; contains_case s2
+  | C.Swhile (_,s1)
+  | C.Sdowhile (s1,_) -> contains_case s1
+  | C.Sfor (s1,e,s2,s3) ->  contains_case s1; contains_case s2; contains_case s3
+  | C.Slabeled(C.Scase _, _) ->
+      unsupported "'case' outside of 'switch'"
+  | C.Slabeled(_,s) -> contains_case s
+  | C.Sblock b -> List.iter contains_case b
+
 (** Annotations for line numbers *)
 
 let add_lineno prev_loc this_loc s =
@@ -953,7 +975,10 @@ let rec convertStmt ploc env s =
   | C.Sswitch(e, s1) ->
       let (init, cases) = groupSwitch (flattenSwitch s1) in
       if init.sdesc <> C.Sskip then
-        warning "ignored code at beginning of 'switch'";
+        begin
+          warning "ignored code at beginning of 'switch'";
+          contains_case init
+        end;
       let te = convertExpr env e in
       add_lineno ploc s.sloc
         (swrap (Ctyping.sswitch te

cparser/Elab.ml

@@ -1817,6 +1817,7 @@ let enter_or_refine_ident local loc env s sto ty =
 	   error loc "static redefinition of '%s' after non-static definition" s; sto
 	| Storage_static,_ -> Storage_static (* Static stays static *)
 	| Storage_extern,_ -> sto
+        | Storage_default,Storage_extern -> Storage_extern
 	| _,Storage_extern -> old_sto
 	| _,Storage_register
 	| Storage_register,_ -> Storage_register

driver/Driver.ml

@@ -74,7 +74,7 @@ let print_error oc msg =
 let output_filename ?(final = false) source_file source_suffix output_suffix =
   match !option_o with
   | Some file when final -> file
-  | _ -> 
+  | _ ->
     Filename.basename (Filename.chop_suffix source_file source_suffix)
     ^ output_suffix
 
@@ -127,7 +127,7 @@ let parse_c_file sourcename ifile =
     let oc = open_out ofile in
     Cprint.program (Format.formatter_of_out_channel oc) ast;
     close_out oc
-  end; 
+  end;
   (* Conversion to Csyntax *)
   let csyntax =
     match Timing.time "CompCert C generation" C2C.convertProgram ast with
@@ -176,7 +176,7 @@ let compile_c_ast sourcename csyntax ofile debug =
     | Errors.Error msg ->
         print_error stderr msg;
         exit 2 in
-  (* Dump Asm in binary format *)  
+  (* Dump Asm in binary format *)
   if !option_sdump then
     dump_asm asm (output_filename sourcename ".c" ".sdump");
   (* Print Asm in text form *)
@@ -219,7 +219,7 @@ let compile_cminor_file ifile ofile =
          eprintf "File %s, character %d: Syntax error\n"
                  ifile (Lexing.lexeme_start lb);
          exit 2
-     | CMlexer.Error msg ->  
+     | CMlexer.Error msg ->
          eprintf "File %s, character %d: %s\n"
                  ifile (Lexing.lexeme_start lb) msg;
          exit 2
@@ -361,7 +361,7 @@ let process_h_file sourcename =
   end else begin
     eprintf "Error: input file %s ignored (not in -E mode)\n" sourcename;
     exit 2
-  end    
+  end
 
 (* Record actions to be performed after parsing the command line *)
 
@@ -386,9 +386,12 @@ let explode_comma_option s =
   | [] -> assert false
   | hd :: tl -> tl
 
+let version_string =
+  "The CompCert C verified compiler, version "^ Configuration.version ^ "\n"
+
 let usage_string =
-"The CompCert C verified compiler, version " ^ Configuration.version ^ "
-Usage: ccomp [options] <source files>
+  version_string ^
+  "Usage: ccomp [options] <source files>
 Recognized source files:
   .c             C source file
   .i or .p       C source file that should not be preprocessed
@@ -464,6 +467,7 @@ General options:
   -stdlib <dir>  Set the path of the Compcert run-time library
   -v             Print external commands before invoking them
   -timings       Show the time spent in various compiler passes
+  -version       Print the version string and exit
 Interpreter mode:
   -interp        Execute given .c files using the reference interpreter
   -quiet         Suppress diagnostic messages for the interpreter
@@ -475,6 +479,9 @@ Interpreter mode:
 let print_usage_and_exit _ =
   printf "%s" usage_string; exit 0
 
+let print_version_and_exit _ =
+  printf "%s" version_string; exit 0
+
 let language_support_options = [
   option_fbitfields; option_flongdouble;
   option_fstruct_return; option_fvararg_calls; option_funprototyped;
@@ -497,13 +504,16 @@ let cmdline_actions =
 (* Getting help *)
   Exact "-help", Self print_usage_and_exit;
   Exact "--help", Self print_usage_and_exit;
+(* Getting version info *)
+  Exact "-version", Self print_version_and_exit;
+  Exact "--version", Self print_version_and_exit;
 (* Processing options *)
   Exact "-c", Set option_c;
   Exact "-E", Set option_E;
   Exact "-S", Set option_S;
   Exact "-o", String(fun s -> option_o := Some s);
   Prefix "-o", Self (fun s -> let s = String.sub s 2 ((String.length s) - 2) in
-			      option_o := Some s);
+                              option_o := Some s);
 (* Preprocessing options *)
   Exact "-I", String(fun s -> prepro_options := s :: "-I" :: !prepro_options);
   Prefix "-I", Self(fun s -> prepro_options := s :: !prepro_options);
@@ -549,7 +559,7 @@ let cmdline_actions =
   Exact "-dmach", Set option_dmach;
   Exact "-dasm", Set option_dasm;
   Exact "-sdump", Set option_sdump;
-(* General options *) 
+(* General options *)
   Exact "-v", Set option_v;
   Exact "-stdlib", String(fun s -> stdlib_path := s);
   Exact "-timings", Set option_timings;

runtime/include/stddef.h

@@ -38,6 +38,14 @@
 #define _STDDEF_H
 #endif
 
+#ifdef __DCC__
+#if !defined(__size_t) && !defined(_SIZE_T)
+#define	__size_t
+#define _SIZE_T
+typedef unsigned int size_t;
+#endif
+#undef __need_size_t
+#else
 #if defined(_STDDEF_H) || defined(__need_size_t)
 #ifndef _SIZE_T
 #define _SIZE_T
@@ -45,6 +53,7 @@ typedef unsigned long size_t;
 #endif
 #undef __need_size_t
 #endif
+#endif
 
 #if defined(_STDDEF_H) || defined(__need_ptrdiff_t)
 #ifndef _PTRDIFF_T
@@ -54,6 +63,20 @@ typedef signed long ptrdiff_t;
 #undef __need_ptrdiff_t
 #endif
 
+#ifdef __DCC__
+#ifndef _WCHART
+#define _WCHART
+#ifndef	__wchar_t
+#define	__wchar_t
+#ifdef _TYPE_wchar_t
+_TYPE_wchar_t;
+#else
+typedef signed int wchar_t;
+#endif
+#endif
+#undef __need_wchar_t
+#endif
+#else
 #if defined(_STDDEF_H) || defined(__need_wchar_t)
 #ifndef _WCHAR_T
 #define _WCHAR_T
@@ -65,6 +88,7 @@ typedef signed int wchar_t;
 #endif
 #undef __need_wchar_t
 #endif
+#endif
 
 #if defined(_STDDEF_H) || defined(__need_NULL)
 #ifndef NULL