diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-06-30 14:49:04 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-06-30 14:49:04 +0200 |
commit | d8ed56833c508b5103a900ef04975013bd9ba77b (patch) | |
tree | c6091bfd87a50a0915ce01629cc96cae1686695c | |
parent | bdbf444704c031a37039d4aeb2f19d05550afbd6 (diff) | |
parent | 19fd986669c098333b88758e85ba146c78a281bf (diff) | |
download | compcert-d8ed56833c508b5103a900ef04975013bd9ba77b.tar.gz compcert-d8ed56833c508b5103a900ef04975013bd9ba77b.zip |
Merge branch 'master' of https://github.com/AbsInt/CompCert
-rw-r--r-- | LICENSE | 21 | ||||
-rw-r--r-- | cfrontend/C2C.ml | 27 | ||||
-rw-r--r-- | cparser/Elab.ml | 1 | ||||
-rw-r--r-- | driver/Driver.ml | 28 | ||||
-rw-r--r-- | runtime/include/stddef.h | 24 | ||||
-rw-r--r--[-rwxr-xr-x] | test/compression/arcode.c | 0 | ||||
-rw-r--r--[-rwxr-xr-x] | test/compression/arcode.h | 0 | ||||
-rw-r--r--[-rwxr-xr-x] | test/compression/armain.c | 0 |
8 files changed, 84 insertions, 17 deletions
@@ -1,14 +1,21 @@ 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 diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 71328c71..96a497bc 100644 --- a/cfrontend/C2C.ml +++ b/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 diff --git a/cparser/Elab.ml b/cparser/Elab.ml index aa015b83..d6b79780 100644 --- a/cparser/Elab.ml +++ b/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 diff --git a/driver/Driver.ml b/driver/Driver.ml index 480cf665..805d5405 100644 --- a/driver/Driver.ml +++ b/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; diff --git a/runtime/include/stddef.h b/runtime/include/stddef.h index 3da06c6f..290434f4 100644 --- a/runtime/include/stddef.h +++ b/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 diff --git a/test/compression/arcode.c b/test/compression/arcode.c index f915cc25..f915cc25 100755..100644 --- a/test/compression/arcode.c +++ b/test/compression/arcode.c diff --git a/test/compression/arcode.h b/test/compression/arcode.h index aac32080..aac32080 100755..100644 --- a/test/compression/arcode.h +++ b/test/compression/arcode.h diff --git a/test/compression/armain.c b/test/compression/armain.c index 8f37c4ff..8f37c4ff 100755..100644 --- a/test/compression/armain.c +++ b/test/compression/armain.c |