From 21156a2fcf48764762c7f2209fa850024378d83a Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 29 Jul 2016 09:15:36 +0200 Subject: Classified all warnings and added various options. Now each warning either has a name and can be turned on/off, made into an error,etc. or is a warning that always will be triggered. The message of the warnings are similar to the ones emited by gcc/clang and all fit into one line. Furthermore the diagnostics are now colored if colored output is available. Bug 18004 --- cfrontend/C2C.ml | 65 +++--- cfrontend/CPragmas.ml | 2 +- cparser/Bitfields.ml | 2 +- cparser/Cerrors.ml | 262 ++++++++++++++++++++-- cparser/Cerrors.mli | 31 ++- cparser/Cutil.ml | 18 +- cparser/Cutil.mli | 3 + cparser/Elab.ml | 573 ++++++++++++++++++++++++++--------------------- cparser/Env.ml | 10 +- cparser/ExtendedAsm.ml | 23 +- cparser/Lexer.mll | 12 +- cparser/PackedStructs.ml | 28 ++- cparser/Parse.ml | 2 +- cparser/Rename.ml | 3 +- cparser/Unblock.ml | 2 +- driver/Driver.ml | 12 +- 16 files changed, 690 insertions(+), 358 deletions(-) diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index decbf58b..c33449e4 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -115,13 +115,13 @@ let currentLocation = ref Cutil.no_loc let updateLoc l = currentLocation := l let error msg = - Cerrors.error "%aError: %s" Cutil.formatloc !currentLocation msg + Cerrors.error !currentLocation "%s" msg let unsupported msg = - Cerrors.error "%aUnsupported feature: %s" Cutil.formatloc !currentLocation msg + Cerrors.error !currentLocation "unsupported feature: %s" msg -let warning msg = - Cerrors.warning "%aWarning: %s" Cutil.formatloc !currentLocation msg +let warning t msg = + Cerrors.warning !currentLocation t msg let string_of_errmsg msg = let string_of_err = function @@ -357,11 +357,11 @@ let make_builtin_memcpy args = let sz1 = match Initializers.constval !comp_env sz with | Errors.OK(Vint n) -> n - | _ -> error "ill-formed __builtin_memcpy_aligned (3rd argument must be a constant)"; Integers.Int.zero in + | _ -> error "argument 3 of of '__builtin_memcpy_aligned' must be a constant"; Integers.Int.zero in let al1 = match Initializers.constval !comp_env al with | Errors.OK(Vint n) -> n - | _ -> error "ill-formed __builtin_memcpy_aligned (4th argument must be a constant)"; Integers.Int.one in + | _ -> error "argument 4 of of '__builtin_memcpy_aligned' must be a constant"; Integers.Int.one in (* to check: sz1 > 0, al1 divides sz1, al1 = 1|2|4|8 *) (* Issue #28: must decay array types to pointer types *) Ebuiltin(EF_memcpy(sz1, al1), @@ -587,15 +587,15 @@ let z_of_str hex str fst = !res -let checkFloatOverflow f = +let checkFloatOverflow f typ = match f with | Fappli_IEEE.B754_finite _ -> () | Fappli_IEEE.B754_zero _ -> - warning "Floating-point literal is so small that it converts to 0" + warning Cerrors.Literal_range "magnitude of floating-point constant too small for type '%s'" typ | Fappli_IEEE.B754_infinity _ -> - warning "Floating-point literal is so large that it converts to infinity" + warning Cerrors.Literal_range "magnitude of floating-point constant too large for type '%s'" typ | Fappli_IEEE.B754_nan _ -> - warning "Floating-point literal converts to Not-a-Number" + warning Cerrors.Literal_range "floating-point converts converts to 'NaN'" let convertFloat f kind = let mant = z_of_str f.C.hex (f.C.intPart ^ f.C.fracPart) 0 in @@ -621,11 +621,11 @@ let convertFloat f kind = begin match kind with | FFloat -> let f = Float32.from_parsed base mant exp in - checkFloatOverflow f; + checkFloatOverflow f "float"; Ctyping.econst_single f | FDouble | FLongDouble -> let f = Float.from_parsed base mant exp in - checkFloatOverflow f; + checkFloatOverflow f "double"; Ctyping.econst_float f end @@ -655,7 +655,7 @@ let rec convertExpr env e = else Ctyping.econst_int (convertInt i) sg | C.EConst(C.CFloat(f, k)) -> if k = C.FLongDouble && not !Clflags.option_flongdouble then - unsupported "'long double' floating-point literal"; + unsupported "'long double' floating-point constant"; convertFloat f k | C.EConst(C.CStr s) -> let ty = typeStringLiteral s in @@ -717,8 +717,7 @@ let rec convertExpr env e = let e2' = convertExpr env e2 in if Cutil.is_composite_type env e1.etyp && List.mem AVolatile (Cutil.attributes_of_type env e1.etyp) then - warning "assignment to a l-value of volatile composite type. \ - The 'volatile' qualifier is ignored."; + warning Cerrors.Unnamed "assignment to a lvalue of volatile composite type"; ewrap (Ctyping.eassign e1' e2') | C.EBinop((C.Oadd_assign|C.Osub_assign|C.Omul_assign|C.Odiv_assign| C.Omod_assign|C.Oand_assign|C.Oor_assign|C.Oxor_assign| @@ -759,12 +758,12 @@ let rec convertExpr env e = let (kind, args1) = match args with | {edesc = C.EConst(CInt(n,_,_))} :: args1 -> (n, args1) - | _ -> error "ill_formed __builtin_debug"; (0L, args) in + | _ -> error "argument 1 of '__builtin_debug' must be constant"; (0L, args) in let (text, args2) = match args1 with | {edesc = C.EConst(CStr(txt))} :: args2 -> (txt, args2) | {edesc = C.EVar id} :: args2 -> (id.name, args2) - | _ -> error "ill_formed __builtin_debug"; ("", args1) in + | _ -> error "argument 2 of '__builtin_debug' must be either a string or variable"; ("", args1) in let targs2 = convertTypArgs env [] args2 in Ebuiltin( EF_debug(P.of_int64 kind, intern_string text, @@ -779,7 +778,7 @@ let rec convertExpr env e = EF_annot(coqstring_of_camlstring txt, typlist_of_typelist targs1), targs1, convertExprList env args1, convertTyp env e.etyp) | _ -> - error "ill-formed __builtin_annot (first argument must be string literal)"; + error "argument 1 of '__builtin_annot' must be a string"; ezero end @@ -792,7 +791,7 @@ let rec convertExpr env e = Tcons(targ, Tnil), convertExprList env [arg], convertTyp env e.etyp) | _ -> - error "ill-formed __builtin_annot_intval (first argument must be string literal)"; + error "argument 1 of '__builtin_annot_intval' must be a string"; ezero end @@ -839,9 +838,9 @@ let rec convertExpr env e = | Some(tres, targs, va) -> checkFunctionType env tres targs; if targs = None && not !Clflags.option_funprototyped then - unsupported "call to unprototyped function (consider adding option -funprototyped)"; + unsupported "call to unprototyped function (consider adding option [-funprototyped])"; if va && not !Clflags.option_fvararg_calls then - unsupported "call to variable-argument function (consider adding option -fvararg-calls)" + unsupported "call to variable-argument function (consider adding option [-fvararg-calls])" end; ewrap (Ctyping.ecall (convertExpr env fn) (convertExprList env args)) @@ -863,7 +862,7 @@ and convertLvalue env e = let e3' = ewrap (Ctyping.ebinop Oadd e1' e2') in ewrap (Ctyping.ederef e3') | _ -> - error "illegal l-value"; ezero + error "illegal lvalue"; ezero and convertExprList env el = match el with @@ -945,7 +944,7 @@ let rec contains_case s = | 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'" + unsupported "'case' statement not in switch statement" | C.Slabeled(_,s) -> contains_case s | C.Sblock b -> List.iter contains_case b @@ -996,7 +995,7 @@ let rec convertStmt env s = | _ -> Cutil.is_debug_stmt s in if init.sdesc <> C.Sskip && not (init_debug init) then begin - warning "ignored code at beginning of 'switch'"; + warning Cerrors.Unnamed "ignored code at beginning of 'switch'"; contains_case init end; let te = convertExpr env e in @@ -1005,9 +1004,9 @@ let rec convertStmt env s = | C.Slabeled(C.Slabel lbl, s1) -> Slabel(intern_string lbl, convertStmt env s1) | C.Slabeled(C.Scase _, _) -> - unsupported "'case' outside of 'switch'"; Sskip + unsupported "'case' statement not in switch statement"; Sskip | C.Slabeled(C.Sdefault, _) -> - unsupported "'default' outside of 'switch'"; Sskip + unsupported "'default' statement not in switch statement"; Sskip | C.Sgoto lbl -> Sgoto(intern_string lbl) | C.Sreturn None -> @@ -1020,7 +1019,7 @@ let rec convertStmt env s = unsupported "inner declarations"; Sskip | C.Sasm(attrs, txt, outputs, inputs, clobber) -> if not !Clflags.option_finline_asm then - unsupported "inline 'asm' statement (consider adding option -finline-asm)"; + unsupported "inline 'asm' statement (consider adding option [-finline-asm])"; Sdo (convertAsm s.sloc env txt outputs inputs clobber) and convertSwitch env is_64 = function @@ -1034,7 +1033,7 @@ and convertSwitch env is_64 = function None | Case e -> match Ceval.integer_expr env e with - | None -> unsupported "'case' label is not a compile-time integer"; + | None -> unsupported "expression is not an integer constant expression"; None | Some v -> Some (if is_64 then Z.of_uint64 v @@ -1047,7 +1046,7 @@ and convertSwitch env is_64 = function let convertFundef loc env fd = checkFunctionType env fd.fd_ret (Some fd.fd_params); if fd.fd_vararg && not !Clflags.option_fvararg_calls then - unsupported "variable-argument function (consider adding option -fvararg-calls)"; + unsupported "variable-argument function (consider adding option [-fvararg-calls])"; let ret = convertTyp env fd.fd_ret in let params = @@ -1132,7 +1131,7 @@ let convertInitializer env ty i = with | Errors.OK init -> init | Errors.Error msg -> - error (sprintf "Initializer is not a compile-time constant (%s)" + error (sprintf "initializer element is not a compile-time constant (%s)" (string_of_errmsg msg)); [] (** Global variable *) @@ -1185,7 +1184,7 @@ let rec convertGlobdecls env res gl = begin match Cutil.unroll env ty with | TFun(tres, targs, va, a) -> if targs = None then - warning ("'" ^ id.name ^ "' is declared without a function prototype"); + warning Cerrors.Unnamed "'%s' is declared without a function prototype" id.name; convertGlobdecls env (convertFundecl env d :: res) gl' | _ -> convertGlobdecls env (convertGlobvar g.gloc env d :: res) gl' @@ -1199,7 +1198,7 @@ let rec convertGlobdecls env res gl = convertGlobdecls env res gl' | C.Gpragma s -> if not (!process_pragma_hook s) then - warning ("'#pragma " ^ s ^ "' directive ignored"); + warning Cerrors.Unknown_pragmas "unknown pragma ignored"; convertGlobdecls env res gl' (** Convert struct and union declarations. @@ -1308,7 +1307,7 @@ let convertProgram p = let typs = convertCompositedefs env [] p in match build_composite_env typs with | Errors.Error msg -> - error (sprintf "Incorrect struct or union definition: %s" + error (sprintf "incorrect struct or union definition: %s" (string_of_errmsg msg)); None | Errors.OK ce -> diff --git a/cfrontend/CPragmas.ml b/cfrontend/CPragmas.ml index 0c932170..2a199ff8 100644 --- a/cfrontend/CPragmas.ml +++ b/cfrontend/CPragmas.ml @@ -73,7 +73,7 @@ let process_pragma name = | "section" :: _ -> C2C.error "ill-formed `section' pragma"; true | "use_section" :: classname :: identlist -> - if identlist = [] then C2C.warning "vacuous `use_section' pragma"; + if identlist = [] then C2C.warning Cerrors.Unnamed "empty `use_section' pragma"; List.iter (process_use_section_pragma classname) identlist; true | "use_section" :: _ -> diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml index d55a6d36..4ff4b94c 100644 --- a/cparser/Bitfields.ml +++ b/cparser/Bitfields.ml @@ -67,7 +67,7 @@ let is_signed_enum_bitfield env sid fld eid n = else if List.for_all (fun (_, v, _) -> int_representable v n true) info.Env.ei_members then true else begin - Cerrors.warning "Warning: not all values of type 'enum %s' can be represented in bit-field '%s' of struct '%s' (%d bits are not enough)" eid.name fld sid.C.name n; + Cerrors.warning Cutil.no_loc Cerrors.Unnamed "warning: '%s' is narrower than values of its type" fld; false end diff --git a/cparser/Cerrors.ml b/cparser/Cerrors.ml index 5c077f37..f2794a2c 100644 --- a/cparser/Cerrors.ml +++ b/cparser/Cerrors.ml @@ -16,8 +16,11 @@ (* Management of errors and warnings *) open Format +open Commandline let warn_error = ref false +let error_fatal = ref false +let color_diagnostics = ref true let num_errors = ref 0 let num_warnings = ref 0 @@ -30,7 +33,7 @@ exception Abort to print its message, as opposed to [Format], and does not automatically introduce indentation and a final dot into the message. This is useful for multi-line messages. *) - + let fatal_error_raw fmt = incr num_errors; Printf.kfprintf @@ -38,23 +41,215 @@ let fatal_error_raw fmt = stderr (fmt ^^ "Fatal error; compilation aborted.\n%!") -let fatal_error fmt = +type msg_class = + | WarningMsg + | ErrorMsg + | FatalErrorMsg + | SuppressedMsg + +type warning_type = + | Unnamed + | Unknown_attribute + | Zero_length_array + | Celeven_extension + | Gnu_empty_struct + | Missing_declarations + | Constant_conversion + | Int_conversion + | Varargs + | Implicit_function_declaration + | Pointer_type_mismatch + | Compare_distinct_pointer_types + | Pedantic + | Main_return_type + | Invalid_noreturn + | Return_type + | Literal_range + | Unknown_pragmas + +let active_warnings: warning_type list ref = ref [ + Unknown_attribute; + Celeven_extension; + Gnu_empty_struct; + Missing_declarations; + Constant_conversion; + Int_conversion; + Varargs; + Implicit_function_declaration; + Pointer_type_mismatch; + Compare_distinct_pointer_types; + Main_return_type; + Invalid_noreturn; + Return_type; + Literal_range; +] + +let error_warnings: warning_type list ref = ref [] + +let string_of_warning = function + | Unnamed -> "" + | Unknown_attribute -> "unknown-attributes" + | Zero_length_array -> "zero-length-array" + | Celeven_extension -> "c11-extensions" + | Gnu_empty_struct -> "gnu-empty-struct" + | Missing_declarations -> "missing-declarations" + | Constant_conversion -> "constant_conversion" + | Int_conversion -> "int-conversion" + | Varargs -> "varargs" + | Implicit_function_declaration -> "implicit-function-declaration" + | Pointer_type_mismatch -> "pointer-type-mismatch" + | Compare_distinct_pointer_types -> "compare-distinct-pointer-types" + | Pedantic -> "pedantic" + | Main_return_type -> "main-return-type" + | Invalid_noreturn -> "invalid-noreturn" + | Return_type -> "return-type" + | Literal_range -> "literal-range" + | Unknown_pragmas -> "unknown-pragmas" + +let activate_warning w = + if not (List.mem w !active_warnings) then + active_warnings:=w::!active_warnings + +let deactivate_warning w = + active_warnings:=List.filter ((<>) w) !active_warnings; + error_warnings:= List.filter ((<>) w) !error_warnings + +let warning_as_error w = + activate_warning w; + if not (List.mem w !error_warnings) then + error_warnings := w::!error_warnings + +let warning_not_as_error w = + error_warnings:= List.filter ((<>) w) !error_warnings + +let wall () = + active_warnings:=[ + Unnamed; + Unknown_attribute; + Zero_length_array; + Celeven_extension; + Gnu_empty_struct; + Missing_declarations; + Constant_conversion; + Int_conversion; + Varargs; + Implicit_function_declaration; + Pointer_type_mismatch; + Compare_distinct_pointer_types; + Pedantic; + Main_return_type; + Invalid_noreturn; + Return_type; + Literal_range; + Unknown_pragmas; + ] + +let werror () = + error_warnings:=[ + Unnamed; + Unknown_attribute; + Zero_length_array; + Celeven_extension; + Gnu_empty_struct; + Missing_declarations; + Constant_conversion; + Int_conversion; + Varargs; + Implicit_function_declaration; + Pointer_type_mismatch; + Compare_distinct_pointer_types; + Pedantic; + Main_return_type; + Invalid_noreturn; + Return_type; + Literal_range; + Unknown_pragmas; + ] + + +let key_of_warning w = + match w with + | Unnamed -> None + | _ -> Some ("-W"^(string_of_warning w)) + +let key_add_werror = function + | None -> Some ("-Werror") + | Some s -> Some ("-Werror,"^s) + +let classify_warning w = + let key = key_of_warning w in + if List.mem w !active_warnings then + if List.mem w !error_warnings then + let key = key_add_werror key in + if !error_fatal then + FatalErrorMsg,key + else + ErrorMsg,key + else + WarningMsg,key + else + SuppressedMsg,None + +let cprintf fmt c = + if Unix.isatty Unix.stderr && !color_diagnostics then + fprintf fmt c + else + ifprintf fmt c + +let rsc fmt = + cprintf fmt "\x1b[0m" + +let bc fmt = + cprintf fmt "\x1b[1m" + +let rc fmt = + cprintf fmt "\x1b[31;1m" + +let mc fmt = + cprintf fmt "\x1b35;1m" + +let pp_key key fmt = + let key = match key with + | None -> "" + | Some s -> " ["^s^"]" in + fprintf fmt "%s%t@." key rsc + +let pp_loc fmt (filename,lineno) = + if filename <> "" then + fprintf fmt "%t%s:%d:%t" bc filename lineno rsc + +let error key loc fmt = incr num_errors; - kfprintf - (fun _ -> raise Abort) - err_formatter - ("@[" ^^ fmt ^^ ".@]@.@[Fatal error; compilation aborted.@]@.") + kfprintf (pp_key key) + err_formatter ("%a %terror:%t: %t" ^^ fmt) pp_loc loc rc rsc bc -let error fmt = +let fatal_error key loc fmt = incr num_errors; - eprintf ("@[" ^^ fmt ^^ ".@]@.") + kfprintf + (fun fmt -> pp_key key fmt;raise Abort) + err_formatter ("%a %terror:%t: %t" ^^ fmt) pp_loc loc rc rsc bc + +let warning loc ty fmt = + let kind,key = classify_warning ty in + match kind with + | ErrorMsg -> + error key loc fmt + | FatalErrorMsg -> + fatal_error key loc fmt + | WarningMsg -> + incr num_warnings; + kfprintf (pp_key key) + err_formatter ("%a %twarning:%tm: %t" ^^ fmt) pp_loc loc mc rsc bc + | SuppressedMsg -> ifprintf err_formatter fmt -let warning fmt = - incr num_warnings; - eprintf ("@[" ^^ fmt ^^ ".@]@.") +let error loc fmt = + if !error_fatal then + fatal_error None loc fmt + else + error None loc fmt -let info fmt = - eprintf ("@[" ^^ fmt ^^ ".@]@.") +let fatal_error loc fmt = + fatal_error None loc fmt let check_errors () = if !num_errors > 0 then @@ -67,4 +262,45 @@ let check_errors () = (if !num_warnings = 1 then "" else "s"); !num_errors > 0 || (!warn_error && !num_warnings > 0) +let error_option w = + let key = string_of_warning w in + [Exact ("-W"^key), Self (fun _ -> activate_warning w); + Exact ("-Wno"^key), Self (fun _ -> deactivate_warning w); + Exact ("-Werror="^key), Self (fun _ -> warning_as_error w); + Exact ("-Wno-error="^key), Self (fun _ -> warning_not_as_error w)] + +let warning_options = + error_option Unnamed @ + error_option Unknown_attribute @ + error_option Zero_length_array @ + error_option Celeven_extension @ + error_option Gnu_empty_struct @ + error_option Missing_declarations @ + error_option Constant_conversion @ + error_option Int_conversion @ + error_option Varargs @ + error_option Implicit_function_declaration @ + error_option Pointer_type_mismatch @ + error_option Compare_distinct_pointer_types @ + error_option Pedantic @ + error_option Main_return_type @ + error_option Invalid_noreturn @ + error_option Return_type @ + error_option Literal_range @ + error_option Unknown_pragmas @ + [Exact ("-Wfatal-errors"), Set error_fatal; + Exact ("-fdiagnostics-color"), Set color_diagnostics; + Exact ("-fno-diagnostics-color"), Unset color_diagnostics; + Exact ("-Werror"), Self (fun _ -> werror ()); + Exact ("-Wall"), Self (fun _ -> wall());] +let warning_help = "Diagnostic options:\n\ +\ -W Enable the specific \n\ +\ -Wno- Disable the specific \n\ +\ -Werror Make all warnings into errors\n\ +\ -Werror= Turn into an error\n\ +\ -Wno-error= Turn into a warning even if -Werror is\n\ + specified\n\ +\ -Wfatal-errors Turn all errors into fatal errors aborting the compilation\n\ +\ -fdiagnostics-color Turn on colored diagnostics\n\ +\ -fno-diagnostics-color Turn of colored diagnostics\n" diff --git a/cparser/Cerrors.mli b/cparser/Cerrors.mli index 3e315fad..3010241a 100644 --- a/cparser/Cerrors.mli +++ b/cparser/Cerrors.mli @@ -17,8 +17,31 @@ val warn_error : bool ref val reset : unit -> unit exception Abort val fatal_error_raw : ('a, out_channel, unit, 'b) format4 -> 'a -val fatal_error : ('a, Format.formatter, unit, unit, unit, 'b) format6 -> 'a -val error : ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a -val warning : ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a -val info : ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a val check_errors : unit -> bool + +type warning_type = + | Unnamed + | Unknown_attribute + | Zero_length_array + | Celeven_extension + | Gnu_empty_struct + | Missing_declarations + | Constant_conversion + | Int_conversion + | Varargs + | Implicit_function_declaration + | Pointer_type_mismatch + | Compare_distinct_pointer_types + | Pedantic + | Main_return_type + | Invalid_noreturn + | Return_type + | Literal_range + | Unknown_pragmas + +val warning : (string * int) -> warning_type -> ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a +val error : (string * int) -> ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a +val fatal_error : (string * int) -> ('a, Format.formatter, unit, unit, unit, 'b) format6 -> 'a + +val warning_help : string +val warning_options : (Commandline.pattern * Commandline.action) list diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index 4b4e1b81..b19b1e4b 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -20,6 +20,11 @@ open C open Env open Machine + +(* Empty location *) + +let no_loc = ("", -1) + (* Set and Map structures over identifiers *) module Ident = struct @@ -478,7 +483,7 @@ let rec sizeof env t = | Some s -> match cautious_mul n s with | Some sz -> Some sz - | None -> error "sizeof(%a) overflows" Cprint.typ t'; Some 1 + | None -> error no_loc "sizeof(%a) overflows" Cprint.typ t'; Some 1 end | TFun(_, _, _, _) -> !config.sizeof_fun | TNamed(_, _) -> sizeof env (unroll env t) @@ -941,6 +946,13 @@ let valid_cast env tfrom tto = | TUnion(s1, _), TUnion(s2, _) -> s1 = s2 | _, _ -> false +(* Check that a cast from the first type to the second is an integer conversion *) + +let int_pointer_conversion env tfrom tto = + match unroll env tfrom, unroll env tto with + | (TInt _ | TEnum _),(TPtr _) -> true + | _,_ -> false + (* Construct an integer constant *) let intconst v ik = @@ -1007,10 +1019,6 @@ let sseq loc s1 s2 = let sassign loc lv rv = { sdesc = Sdo (eassign lv rv); sloc = loc } -(* Empty location *) - -let no_loc = ("", -1) - (* Dummy skip statement *) let sskip = { sdesc = Sskip; sloc = no_loc } diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index 91b073ab..b724f573 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -198,6 +198,9 @@ val valid_assignment : Env.t -> exp -> typ -> bool the given type is allowed. *) val valid_cast : Env.t -> typ -> typ -> bool (* Check that a cast from the first type to the second is allowed. *) +val int_pointer_conversion: Env.t -> typ -> typ -> bool + (* Check that a cast from the first type to the second is an integer + conversion *) val fundef_typ: fundef -> typ (* Return the function type for the given function definition. *) val int_representable: int64 -> int -> bool -> bool diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 76f8efdb..e3a0ef0c 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -22,6 +22,7 @@ open Machine open !Cabs open Cabshelper open !C +open Cerrors open Cutil open Env @@ -30,13 +31,19 @@ open Env (* Error reporting *) let fatal_error loc fmt = - Cerrors.fatal_error ("%a: Error:@ " ^^ fmt) format_cabsloc loc + fatal_error (loc.filename,loc.lineno) fmt let error loc fmt = - Cerrors.error ("%a: Error:@ " ^^ fmt) format_cabsloc loc + error (loc.filename,loc.lineno) fmt -let warning loc fmt = - Cerrors.warning ("%a: Warning:@ " ^^ fmt) format_cabsloc loc +let warning loc = + warning (loc.filename,loc.lineno) + +let print_typ env fmt ty = + match ty with + | TNamed _ -> + Format.fprintf fmt "'%a' (aka '%a')" Cprint.typ ty Cprint.typ (Cutil.unroll env ty) + | _ -> Format.fprintf fmt "'%a'" Cprint.typ ty (* Error reporting for Env functions *) @@ -115,12 +122,9 @@ let combine_toplevel_definitions loc env s old_sto old_ty sto ty = | Some new_ty -> new_ty | None -> - let id = Env.fresh_ident s in error loc - "redefinition of '%s' with incompatible type.@ \ - Previous declaration: %a.@ \ - New declaration: %a" - s Cprint.simple_decl (id, old_ty) Cprint.simple_decl (id, ty); + "redefinition of '%s' with a different type: %a vs %a" + s (print_typ env) old_ty (print_typ env) ty; ty in let new_sto = (* The only case not allowed is removing static *) @@ -130,8 +134,8 @@ let combine_toplevel_definitions loc env s old_sto old_ty sto ty = | Storage_register,Storage_register | Storage_default,Storage_default -> sto | _,Storage_static -> - error loc "static redefinition of '%s' after non-static definition" s; - sto + error loc "static declaration of '%s' follows non-static declaration" s; + sto | Storage_static,_ -> Storage_static (* Static stays static *) | Storage_extern,_ -> sto | Storage_default,Storage_extern -> Storage_extern @@ -149,14 +153,14 @@ let enter_or_refine_ident local loc env s sto ty = - an enum that was already declared in the same scope. Redefinition of a variable at global scope (or extern) is treated below. *) if redef Env.lookup_typedef env s then - error loc "redefinition of typedef '%s' as different kind of symbol" s; + error loc "redefinition of '%s' as different kind of symbol" s; begin match previous_def Env.lookup_ident env s with | Some(id, II_ident(old_sto, old_ty)) when local && Env.in_current_scope env id && not (sto = Storage_extern && old_sto = Storage_extern) -> - error loc "redefinition of local variable '%s'" s + error loc "redefinition of '%s'" s | Some(id, II_enum _) when Env.in_current_scope env id -> - error loc "redefinition of enumerator '%s'" s + error loc "redefinition of '%s' as different kind of symbol" s; | _ -> () end; @@ -277,7 +281,7 @@ let elab_int_constant loc s0 = try parse_int base s with | Overflow -> - error loc "integer literal '%s' is too large" s0; + error loc "integer literal '%s' is too large to be represented in any integer type" s0; 0L | Bad_digit -> (*error loc "bad digit in integer literal '%s'" s0;*) (* Is caught earlier *) @@ -313,17 +317,23 @@ let elab_char_constant loc wide chars = (* Treat multi-char constants as a number in base 2^nbits *) let max_digit = Int64.shift_left 1L nbits in let max_val = Int64.shift_left 1L (64 - nbits) in - let v = + let v,_ = List.fold_left - (fun acc d -> - if acc < 0L || acc >= max_val then - error loc "character constant overflows"; - if d < 0L || d >= max_digit then - error loc "escape sequence is out of range (code 0x%LX)" d; - Int64.add (Int64.shift_left acc nbits) d) - 0L chars in + (fun (acc,err) d -> + if not err then begin + let overflow = acc < 0L || acc >= max_val + and out_of_range = d < 0L || d >= max_digit in + if overflow then + error loc "character constant too long for its type"; + if out_of_range then + error loc "escape sequence is out of range (code 0x%LX)" d; + Int64.add (Int64.shift_left acc nbits) d,overflow || out_of_range + end else + Int64.add (Int64.shift_left acc nbits) d,true + ) + (0L,false) chars in if not (integer_representable v IInt) then - warning loc "character constant cannot be represented at type 'int'"; + warning loc Unnamed "character constant too long for its type"; (* C99 6.4.4.4 item 10: single character -> represent at type char or wchar_t *) Ceval.normalize_int v @@ -365,7 +375,7 @@ let elab_constant loc = function let elab_simple_string loc wide chars = match elab_string_literal loc wide chars with | CStr s -> s - | _ -> error loc "wide character string not allowed here"; "" + | _ -> error loc "cannot use wide string literal in 'asm'"; "" (** * Elaboration of type expressions, type specifiers, name declarations *) @@ -406,7 +416,8 @@ let elab_gcc_attr loc env = function begin try [Attr(v, List.map (elab_attr_arg loc env) args)] with Wrong_attr_arg -> - warning loc "cannot parse '%s' attribute, ignored" v; [] + warning loc Unknown_attribute + "unknown attribute '%s' ignored" v; [] end let is_power_of_two n = n > 0L && Int64.logand n (Int64.pred n) = 0L @@ -415,8 +426,10 @@ let extract_alignas loc a = match a with | Attr(("aligned"|"__aligned__"), args) -> begin match args with - | [AInt n] when is_power_of_two n -> AAlignas (Int64.to_int n) - | _ -> warning loc "bad 'aligned' attribute, ignored"; a + | [AInt n] when is_power_of_two n -> AAlignas (Int64.to_int n) + | [AInt n] -> error loc "requested alignment is not a power of 2"; a + | [_] -> error loc "requested alignment is not an integer constant"; a + | _ -> error loc "'aligned' attribute takes no more than 1 argument"; a end | _ -> a @@ -431,11 +444,16 @@ let elab_attribute env = function [Attr("__packed__", List.map (elab_attr_arg loc env) args)] | ALIGNAS_ATTR ([a], loc) -> begin match elab_attr_arg loc env a with - | AInt n when is_power_of_two n -> [AAlignas (Int64.to_int n)] - | _ -> warning loc "bad _Alignas value, ignored"; [] + | AInt n -> + if is_power_of_two n then + [AAlignas (Int64.to_int n)] + else begin + error loc "requested alignment is not a power of 2"; [] + end + | _ -> error loc "requested alignment is not an integer constant"; [] end | ALIGNAS_ATTR (_, loc) -> - warning loc "_Alignas takes exactly one parameter, ignored"; [] + error loc "_Alignas takes no more than 1 argument"; [] let elab_attributes env al = List.fold_left add_attributes [] (List.map (elab_attribute env) al) @@ -489,7 +507,7 @@ let rec elab_specifier ?(only = false) loc env specifier = attr := add_attributes (elab_cvspec env cv) !attr | SpecStorage st -> if !sto <> Storage_default && st <> TYPEDEF then - error loc "multiple storage specifiers"; + error loc "multiple storage classes in declaration specifiers"; begin match st with | AUTO -> () | STATIC -> sto := Storage_static @@ -609,6 +627,13 @@ and elab_cvspecs env cv_specs = List.fold_left add_attributes [] (List.map (elab_cvspec env) cv_specs) (* Elaboration of a type declarator. C99 section 6.7.5. *) +and elab_return_type loc env ty = + match unroll env ty with + | TArray _ -> + error loc "function cannot return array type %a" (print_typ env) ty + | TFun _ -> + error loc "function cannot return function type %a" (print_typ env) ty + | _ -> () and elab_type_declarator loc env ty kr_ok = function | Cabs.JUSTBASE -> @@ -623,36 +648,29 @@ and elab_type_declarator loc env ty kr_ok = function let expr,env = (!elab_expr_f loc env sz) in match Ceval.integer_expr env expr with | Some n -> - if n < 0L then error loc "array size is negative"; - if n = 0L then warning loc "array of size 0"; + if n < 0L then error loc "size of array is negative"; + if n = 0L then warning loc Zero_length_array + "zero size arrays are an extension"; Some n | None -> - error loc "array size is not a compile-time constant"; + error loc "size of array is not a compile-time constant"; Some 1L in (* produces better error messages later *) elab_type_declarator loc env (TArray(ty, sz', a)) kr_ok d | Cabs.PTR(cv_specs, d) -> let a = elab_cvspecs env cv_specs in elab_type_declarator loc env (TPtr(ty, a)) kr_ok d | Cabs.PROTO(d, (params, vararg)) -> - begin match unroll env ty with - | TArray _ | TFun _ -> - error loc "Illegal function return type@ %a" Cprint.typ ty - | _ -> () - end; + elab_return_type loc env ty; let params' = elab_parameters env params in elab_type_declarator loc env (TFun(ty, Some params', vararg, [])) kr_ok d | Cabs.PROTO_OLD(d, params) -> - begin match unroll env ty with - | TArray _ | TFun _ -> - error loc "Illegal function return type@ %a" Cprint.typ ty - | _ -> () - end; + elab_return_type loc env ty; match params with | [] -> elab_type_declarator loc env (TFun(ty, None, false, [])) kr_ok d | _ -> if not kr_ok || d <> Cabs.JUSTBASE then - fatal_error loc "Illegal old-style K&R function definition"; + fatal_error loc "illegal old-style K&R function definition"; ((TFun(ty, None, false, []), Some params), env) (* Elaboration of parameters in a prototype *) @@ -675,7 +693,7 @@ and elab_parameter env (PARAM (spec, id, decl, attr, loc)) = let ty = add_attributes_type (elab_attributes env attr) ty in if sto <> Storage_default && sto <> Storage_register then error loc - "'extern' or 'static' storage not supported for function parameter"; + "invalid storage class specifier in function declarator"; if inl then error loc "'inline' can only appear on functions"; if noret then @@ -750,9 +768,10 @@ 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 - warning loc "ISO C99 does not support anonymous structs/unions" + warning loc Celeven_extension "anonymous structs/unions are a C11 extension" else - warning loc "declaration does not declare any members"; + (* This should actually never be triggered, empty structs are captured earlier *) + warning loc Missing_declarations "declaration does not declare anything"; let elab_bitfield (Name (_, _, _, loc), optbitsize) (id, ty) = let optbitsize' = @@ -766,28 +785,28 @@ and elab_field_group env (Field_group (spec, fieldlist, loc)) = | _ -> ILongLong (* trigger next error message *) in if integer_rank ik > integer_rank IInt then begin error loc - "the type of bitfield '%s' must be an integer type \ - no bigger than 'int'" id; + "the type of bitfield '%s' must be an integer type no bigger than 'int'" id; None end else begin let expr,env' =(!elab_expr_f loc env sz) in match Ceval.integer_expr env' expr with | Some n -> if n < 0L then begin - error loc "bit size of '%s' (%Ld) is negative" id n; + error loc "bit-filed '%s' has negative width (%Ld)" id n; None end else - if n > Int64.of_int(sizeof_ikind ik * 8) then begin - error loc "bit size of '%s' (%Ld) exceeds its type" id n; - None + let max = Int64.of_int(sizeof_ikind ik * 8) in + if n > max then begin + error loc "size of bit-field '%s' (%Ld bits) exceeds its type (%Ld bits)" id n max; + None end else if n = 0L && id <> "" then begin - error loc "member '%s' has zero size" id; + error loc "named bit-field '%s' has zero width" id; None end else Some(Int64.to_int n) | None -> - error loc "bit size of '%s' is not a compile-time constant" id; + error loc "bit-field '%s' witdth not an integer constant" id; None end in { fld_name = id; fld_typ = ty; fld_bitfield = optbitsize' } @@ -812,13 +831,13 @@ and elab_struct_or_union_info kind loc env members attrs = check_incomplete m; (* Warn for empty structs or unions *) if m = [] then - warning loc "empty %s" (if kind = Struct then "struct" else "union"); + warning loc Celeven_extension "anonymous %s are an extension" (if kind = Struct then "struct" else "union"); (composite_info_def env' kind attrs m, env') and elab_struct_or_union only kind loc tag optmembers attrs env = let warn_attrs () = if attrs <> [] then - warning loc "attributes over struct/union ignored in this context" in + warning loc Unnamed "attribute declaration must precede definition" in let optbinding, tag = match tag with | None -> None, "" @@ -833,12 +852,14 @@ and elab_struct_or_union only kind loc tag optmembers attrs env = and the composite was bound in another scope, create a new incomplete composite instead via the case "_, None" below. *) + if ci.ci_kind <> kind then + error loc "use of '%s' with tag type that does not match previous declaration" tag; warn_attrs(); (tag', env) | Some(tag', ({ci_sizeof = None} as ci)), Some members when Env.in_current_scope env tag' -> if ci.ci_kind <> kind then - error loc "struct/union mismatch on tag '%s'" tag; + error loc "use of '%s' with tag type that does not match previous declaration" tag; (* finishing the definition of an incomplete struct or union *) let (ci', env') = elab_struct_or_union_info kind loc env members attrs in (* Emit a global definition for it *) @@ -887,15 +908,15 @@ and elab_enum_item env ((s, exp), loc) nextval = | Some n -> (n, Some exp') | None -> error loc - "value of enumerator '%s' is not a compile-time constant" s; + "value of enumerator '%s' is not an integer constant" s; (nextval, Some exp') in if redef Env.lookup_ident env s then - error loc "redefinition of identifier '%s'" s; + error loc "'%s' redeclared as different kind of symbol" s; if redef Env.lookup_typedef env s then - error loc "redefinition of typedef '%s' as different kind of symbol" s; + error loc "'%s' redeclared as different kind of symbol" s; if not (int_representable v (8 * sizeof_ikind enum_ikind) (is_signed_ikind enum_ikind)) then - warning loc "the value of '%s' is not representable with type %a" - s Cprint.typ (TInt(enum_ikind, [])); + warning loc Constant_conversion "integer literal '%Ld' is too large to be represented in any integer type" + v; let (id, env') = Env.enter_enum_item env s v in ((id, v, exp'), Int64.succ v, env') @@ -967,13 +988,18 @@ let init_int_array_wstring opt_size s = let check_init_type loc env a ty = if wrap2 valid_assignment loc env a ty then () else if wrap2 valid_cast loc env a.etyp ty then - warning loc - "initializer has type@ %a@ instead of the expected type @ %a" - Cprint.typ a.etyp Cprint.typ ty + if wrap2 int_pointer_conversion loc env a.etyp ty then + warning loc Int_conversion + "incompatible integer to pointer conversion initializing %a with an expression of type %a" + (print_typ env) ty (print_typ env) a.etyp + else + warning loc Int_conversion + "incompatible pointer to integer conversion initializing %a with an expression of type %a" + (print_typ env) ty (print_typ env) a.etyp else error loc - "initializer has type@ %a@ instead of the expected type @ %a" - Cprint.typ a.etyp Cprint.typ ty + "initializing %a with an expression of incompatible type %a" + (print_typ env) ty (print_typ env) a.etyp (* Representing initialization state using zippers *) @@ -1159,23 +1185,21 @@ let rec elab_designator loc env zi desig = | Some zi' -> elab_designator loc env zi' desig' | None -> - error loc "%s has no member named %s" (I.name zi) name; + error loc "field designator '%s' does not have refer to any field in type '%s'" name (I.name zi); raise Exit end | ATINDEX_INIT a :: desig' -> let expr,env = (!elab_expr_f loc env a) in begin match Ceval.integer_expr env expr with | None -> - error loc "array element designator for %s is not a compile-time constant" - (I.name zi); + error loc "expression is not an integer constant expression"; raise Exit | Some n -> match I.index env zi n with | Some zi' -> elab_designator loc env zi' desig' | None -> - error loc "bad array element designator %Ld within %s" - n (I.name zi); + error loc "array index in initializer exceeds array bounds"; raise Exit end @@ -1198,7 +1222,7 @@ let rec elab_list zi il first = match (if first then I.first env zi else I.next zi) with | None -> - warning loc "excess elements at end of initializer for %s, ignored" + warning loc Unnamed "excess elements in initializer for %s" (I.name zi); I.to_init zi | Some zi' -> @@ -1221,16 +1245,14 @@ and elab_item zi item il = begin match elab_string_literal loc w s, unroll env ty_elt with | CStr s, TInt((IChar | ISChar | IUChar), _) -> if not (I.index_below (Int64.of_int(String.length s - 1)) sz) then - warning loc "initializer string for array of chars %s is too long" - (I.name zi); + warning loc Unnamed "initializer-string for array of chars is too long"; elab_list (I.set zi (init_char_array_string sz s)) il false | CStr _, _ -> error loc "initialization of an array of non-char elements with a string literal"; elab_list zi il false | CWStr s, TInt(_, _) when compatible_types AttrIgnoreTop env ty_elt (TInt(wchar_ikind(), [])) -> if not (I.index_below (Int64.of_int(List.length s - 1)) sz) then - warning loc "initializer string for array of wide chars %s is too long" - (I.name zi); + warning loc Unnamed "initializer string for array of wide chars is too long"; elab_list (I.set zi (init_int_array_wstring sz s)) il false | CWStr _, _ -> error loc "initialization of an array of non-wchar_t elements with a wide string literal"; @@ -1276,8 +1298,8 @@ and elab_single zi a il = raise Exit end | _ -> - error loc "impossible to initialize %s of type@ %a" - (I.name zi) Cprint.typ ty; + error loc "impossible to initialize %s of type %a" + (I.name zi) (print_typ env) ty; raise Exit (* Start with top-level object initialized to default *) @@ -1302,7 +1324,7 @@ let elab_initial loc env root ty ie = let fixup_typ loc env ty init = match unroll env ty, init with | TArray(ty_elt, None, attr), Init_array il -> - if il = [] then warning loc "array of size 0"; + if il = [] then warning loc Zero_length_array "zero size arrays are an extension"; TArray(ty_elt, Some(Int64.of_int(List.length il)), attr) | _ -> ty @@ -1322,7 +1344,18 @@ let elab_expr loc env a = let err fmt = error loc fmt in (* non-fatal error *) let error fmt = fatal_error loc fmt in - let warning fmt = warning loc fmt in + let warning t fmt = + warning loc t fmt in + + let check_ptr_arith env ty = + match unroll env ty with + | TVoid _ -> + err "illegal arithmetic on a pointer to void" + | TFun _ -> + err "illegal arithmetic on a pointer to the function type %a" (print_typ env) ty + | _ -> if incomplete_type env ty then + err "arithmetic on a pointer to an incomplete type %a" (print_typ env) ty + in let rec elab env = function @@ -1349,7 +1382,7 @@ let elab_expr loc env a = match (unroll env b1.etyp, unroll env b2.etyp) with | (TPtr(t, _) | TArray(t, _, _)), (TInt _ | TEnum _) -> t | (TInt _ | TEnum _), (TPtr(t, _) | TArray(t, _, _)) -> t - | t1, t2 -> error "incorrect types for array subscripting" in + | t1, t2 -> error "subscripted value is not an array, or pointer" in { edesc = EBinop(Oindex, b1, b2, TPtr(tres, [])); etyp = tres },env | MEMBEROF(a1, fieldname) -> @@ -1361,7 +1394,7 @@ let elab_expr loc env a = | TUnion(id, attrs) -> (wrap Env.find_union_member loc env (id, fieldname), attrs) | _ -> - error "left-hand side of '.' is not a struct or union" in + error "member reference base type %a is not a structure or union" (print_typ env) b1.etyp in (* A field of a const/volatile struct or union is itself const/volatile *) { edesc = EUnop(Odot fieldname, b1); etyp = add_attributes_type (List.filter attr_inherited_by_members attrs) @@ -1378,10 +1411,10 @@ let elab_expr loc env a = | TUnion(id, attrs) -> (wrap Env.find_union_member loc env (id, fieldname), attrs) | _ -> - error "left-hand side of '->' is not a pointer to a struct or union" + error "member reference base type %a is not a struct or union" (print_typ env) b1.etyp end | _ -> - error "left-hand side of '->' is not a pointer " in + error "member reference type %a is not a pointer" (print_typ env) b1.etyp in { edesc = EUnop(Oarrow fieldname, b1); etyp = add_attributes_type (List.filter attr_inherited_by_members attrs) (type_of_member env fld) },env @@ -1412,9 +1445,8 @@ let elab_expr loc env a = let ty = match b3.edesc with ESizeof ty -> ty | _ -> assert false in let ty' = default_argument_conversion env ty in if not (compatible_types AttrIgnoreTop env ty ty') then - warning "'%a' is promoted to '%a' when passed through '...'.@ You should pass '%a', not '%a', to 'va_arg'" - Cprint.typ ty Cprint.typ ty' - Cprint.typ ty' Cprint.typ ty; + warning Varargs "second argument of va_rarg is of promotable type %a; this var_arg has undefined behavior because arguments will be promoted to %a" + (print_typ env) ty (print_typ env) ty'; { edesc = ECall(ident, [b2; b3]); etyp = ty },env | CALL(a1, al) -> @@ -1423,7 +1455,7 @@ let elab_expr loc env a = having declared it *) match a1 with | VARIABLE n when not (Env.ident_is_bound env n) -> - warning "implicit declaration of function '%s'" n; + warning Implicit_function_declaration "implicit declaration of function '%s' is invalid in C99" n; let ty = TFun(TInt(IInt, []), None, false, []) in (* Check against other definitions and enter in env *) let (id, sto, env, ty, linkage) = @@ -1440,9 +1472,9 @@ let elab_expr loc env a = | TPtr(ty, a) -> begin match unroll env ty with | TFun(res, args, vararg, a) -> (res, args, vararg) - | _ -> error "the function part of a call does not have a function type" + | _ -> error "called object type %a is not a function or function pointer" (print_typ env) b1.etyp end - | _ -> error "the function part of a call does not have a function type" + | _ -> error "called object type %a is not a function or function pointer" (print_typ env) b1.etyp in (* Type-check the arguments against the prototype *) let bl',env = @@ -1452,9 +1484,9 @@ let elab_expr loc env a = { edesc = ECall(b1, bl'); etyp = res },env | UNARY(POSINCR, a1) -> - elab_pre_post_incr_decr Opostincr "postfix '++'" a1 + elab_pre_post_incr_decr Opostincr "increment" a1 | UNARY(POSDECR, a1) -> - elab_pre_post_incr_decr Opostdecr "postfix '--'" a1 + elab_pre_post_incr_decr Opostdecr "decrement" a1 (* 6.5.4 Cast operators *) @@ -1462,7 +1494,21 @@ let elab_expr loc env a = let (ty, _) = elab_type loc env spec dcl in let b1,env = elab env a1 in if not (wrap2 valid_cast loc env b1.etyp ty) then - err "illegal cast from %a@ to %a" Cprint.typ b1.etyp Cprint.typ ty; + begin match unroll env b1.etyp, unroll env ty with + | _, (TStruct _|TUnion _ | TVoid _) -> + err "used type %a where arithmetic or pointer type is required" + (print_typ env) ty + | (TStruct _| TUnion _ | TVoid _),_ -> + err "operand of type %a where arithmetic or pointer type is required" + (print_typ env) b1.etyp + | TFloat _, TPtr _ -> + err "operand of type %a cannot be cast to a pointer typ" + (print_typ env) b1.etyp + | TPtr _ , TFloat _ -> + err "pointer cannot be cast to type %a" (print_typ env) ty + | _ -> + err "illegal cast from %a to %a" (print_typ env) b1.etyp (print_typ env) ty + end; { edesc = ECast(ty, b1); etyp = ty },env (* 6.5.2.5 Compound literals *) @@ -1479,7 +1525,7 @@ let elab_expr loc env a = | EXPR_SIZEOF a1 -> let b1,env = elab env a1 in if wrap incomplete_type loc env b1.etyp then - err "incomplete type %a" Cprint.typ b1.etyp; + err "invalid application of 'sizeof' to an incomplete type %a" (print_typ env) b1.etyp; let bdesc = (* Catch special cases sizeof("string literal") *) match b1.edesc with @@ -1496,49 +1542,49 @@ let elab_expr loc env a = | TYPE_SIZEOF (spec, dcl) -> let (ty, env') = elab_type loc env spec dcl in if wrap incomplete_type loc env' ty then - err "incomplete type %a" Cprint.typ ty; + err "invalid application of 'sizeof' to an incomplete type %a" (print_typ env) ty; { edesc = ESizeof ty; etyp = TInt(size_t_ikind(), []) },env' | EXPR_ALIGNOF a1 -> let b1,env = elab env a1 in if wrap incomplete_type loc env b1.etyp then - err "incomplete type %a" Cprint.typ b1.etyp; + err "invalid application of 'alignof' to an incomplete type %a" (print_typ env) b1.etyp; { edesc = EAlignof b1.etyp; etyp = TInt(size_t_ikind(), []) },env | TYPE_ALIGNOF (spec, dcl) -> let (ty, env') = elab_type loc env spec dcl in if wrap incomplete_type loc env' ty then - err "incomplete type %a" Cprint.typ ty; - { edesc = EAlignof ty; etyp = TInt(size_t_ikind(), []) },env + err "invalid application of 'alignof' to an incomplete type %a" (print_typ env) ty; + { edesc = EAlignof ty; etyp = TInt(size_t_ikind(), []) },env' | UNARY(PLUS, a1) -> let b1,env = elab env a1 in if not (is_arith_type env b1.etyp) then - err "argument of unary '+' is not an arithmetic type"; + error "invalid argument type %a to unary expression" (print_typ env) b1.etyp; { edesc = EUnop(Oplus, b1); etyp = unary_conversion env b1.etyp },env | UNARY(MINUS, a1) -> let b1,env = elab env a1 in if not (is_arith_type env b1.etyp) then - err "argument of unary '-' is not an arithmetic type"; + error "invalid argument type %a to unary expression" (print_typ env) b1.etyp; { edesc = EUnop(Ominus, b1); etyp = unary_conversion env b1.etyp },env | UNARY(BNOT, a1) -> let b1,env = elab env a1 in if not (is_integer_type env b1.etyp) then - err "argument of '~' is not an integer type"; + error "invalid argument type %a to unary expression" (print_typ env) b1.etyp; { edesc = EUnop(Onot, b1); etyp = unary_conversion env b1.etyp },env | UNARY(NOT, a1) -> let b1,env = elab env a1 in if not (is_scalar_type env b1.etyp) then - err "argument of '!' is not a scalar type"; + error "invalid argument type %a to unary expression" (print_typ env) b1.etyp; { edesc = EUnop(Olognot, b1); etyp = TInt(IInt, []) },env | UNARY(ADDROF, a1) -> let b1,env = elab env a1 in if not (is_lvalue b1 || is_function_type env b1.etyp) then - err "argument of '&' is not an l-value"; + err "cannot take the address of an rvalue of type %a" (print_typ env) b1.etyp; begin match b1.edesc with | EVar id -> begin match wrap Env.find_ident loc env id with @@ -1566,24 +1612,25 @@ let elab_expr loc env a = | TPtr(ty, _) | TArray(ty, _, _) -> { edesc = EUnop(Oderef, b1); etyp = ty },env | _ -> - error "argument of unary '*' is not a pointer" + error "indirection requires pointer operand (%a invalid)" + (print_typ env) b1.etyp end | UNARY(PREINCR, a1) -> - elab_pre_post_incr_decr Opreincr "prefix '++'" a1 + elab_pre_post_incr_decr Opreincr "increment" a1 | UNARY(PREDECR, a1) -> - elab_pre_post_incr_decr Opredecr "prefix '--'" a1 + elab_pre_post_incr_decr Opredecr "decrement" a1 (* 6.5.5 to 6.5.12 Binary operator expressions *) | BINARY(MUL, a1, a2) -> - elab_binary_arithmetic "*" Omul a1 a2 + elab_binary_arithmetic Omul a1 a2 | BINARY(DIV, a1, a2) -> - elab_binary_arithmetic "/" Odiv a1 a2 + elab_binary_arithmetic Odiv a1 a2 | BINARY(MOD, a1, a2) -> - elab_binary_integer "/" Omod a1 a2 + elab_binary_integer Omod a1 a2 | BINARY(ADD, a1, a2) -> let b1,env = elab env a1 in @@ -1596,9 +1643,10 @@ let elab_expr loc env a = match unroll env b1.etyp, unroll env b2.etyp with | (TPtr(ty, a) | TArray(ty, _, a)), (TInt _ | TEnum _) -> ty | (TInt _ | TEnum _), (TPtr(ty, a) | TArray(ty, _, a)) -> ty - | _, _ -> error "type error in binary '+'" in - if not (pointer_arithmetic_ok env ty) then - err "illegal pointer arithmetic in binary '+'"; + | _, _ -> error "invalid operands to binary expression (%a and %a)" + (print_typ env) b1.etyp (print_typ env) b2.etyp + in + check_ptr_arith env ty; TPtr(ty, []) end in { edesc = EBinop(Oadd, b1, b2, tyres); etyp = tyres },env @@ -1617,27 +1665,27 @@ let elab_expr loc env a = err "illegal pointer arithmetic in binary '-'"; (TPtr(ty, []), TPtr(ty, [])) | (TInt _ | TEnum _), (TPtr(ty, a) | TArray(ty, _, a)) -> - if not (pointer_arithmetic_ok env ty) then - err "illegal pointer arithmetic in binary '-'"; + check_ptr_arith env ty; (TPtr(ty, []), TPtr(ty, [])) | (TPtr(ty1, a1) | TArray(ty1, _, a1)), (TPtr(ty2, a2) | TArray(ty2, _, a2)) -> if not (compatible_types AttrIgnoreAll env ty1 ty2) then - err "mismatch between pointer types in binary '-'"; - if not (pointer_arithmetic_ok env ty1) then - err "illegal pointer arithmetic in binary '-'"; + err "%a and %a are not pointers to compatible types" + (print_typ env) b1.etyp (print_typ env) b1.etyp; + check_ptr_arith env ty1; if wrap sizeof loc env ty1 = Some 0 then err "subtraction between two pointers to zero-sized objects"; (TPtr(ty1, []), TInt(ptrdiff_t_ikind(), [])) - | _, _ -> error "type error in binary '-'" + | _, _ -> error "invalid operands to binary expression (%a and %a)" + (print_typ env) b1.etyp (print_typ env) b2.etyp end in { edesc = EBinop(Osub, b1, b2, tyop); etyp = tyres },env | BINARY(SHL, a1, a2) -> - elab_shift "<<" Oshl a1 a2 + elab_binary_integer Oshl a1 a2 | BINARY(SHR, a1, a2) -> - elab_shift ">>" Oshr a1 a2 + elab_binary_integer Oshr a1 a2 | BINARY(EQ, a1, a2) -> elab_comparison Oeq a1 a2 @@ -1653,11 +1701,11 @@ let elab_expr loc env a = elab_comparison Oge a1 a2 | BINARY(BAND, a1, a2) -> - elab_binary_integer "&" Oand a1 a2 + elab_binary_integer Oand a1 a2 | BINARY(BOR, a1, a2) -> - elab_binary_integer "|" Oor a1 a2 + elab_binary_integer Oor a1 a2 | BINARY(XOR, a1, a2) -> - elab_binary_integer "^" Oxor a1 a2 + elab_binary_integer Oxor a1 a2 (* 6.5.13 and 6.5.14 Logical operator expressions *) @@ -1672,12 +1720,13 @@ let elab_expr loc env a = let b2,env = elab env a2 in let b3,env = elab env a3 in if not (is_scalar_type env b1.etyp) then - err ("the first argument of '? :' is not a scalar type"); + err "used type %a where arithmetic or pointer type is required" + (print_typ env) b1.etyp; begin match pointer_decay env b2.etyp, pointer_decay env b3.etyp with | (TInt _ | TFloat _ | TEnum _), (TInt _ | TFloat _ | TEnum _) -> { edesc = EConditional(b1, b2, b3); etyp = binary_conversion env b2.etyp b3.etyp },env - | TPtr(ty1, a1), TPtr(ty2, a2) -> + | (TPtr(ty1, a1) as pty1), (TPtr(ty2, a2) as pty2) -> let tyres = if is_void_type env ty1 || is_void_type env ty2 then TPtr(TVoid (add_attributes a1 a2), []) @@ -1685,8 +1734,8 @@ let elab_expr loc env a = match combine_types AttrIgnoreAll env (TPtr(ty1, a1)) (TPtr(ty2, a2)) with | None -> - warning "the second and third arguments of '? :' \ - have incompatible pointer types"; + warning Pointer_type_mismatch "pointer type mismatch (%a and %a)" + (print_typ env) pty1 (print_typ env) pty2; (* tolerance *) TPtr(TVoid (add_attributes a1 a2), []) | Some ty -> ty @@ -1699,7 +1748,8 @@ let elab_expr loc env a = | ty1, ty2 -> match combine_types AttrIgnoreAll env ty1 ty2 with | None -> - error ("the second and third arguments of '? :' have incompatible types") + error "incompatible operand types (%a and %a)" + (print_typ env) ty1 (print_typ env) ty2 | Some tyres -> { edesc = EConditional(b1, b2, b3); etyp = tyres },env end @@ -1710,16 +1760,22 @@ let elab_expr loc env a = let b1,env = elab env a1 in let b2,env = elab env a2 in if List.mem AConst (attributes_of_type env b1.etyp) then - err "left-hand side of assignment has 'const' type"; + error "read-only variable is not assignable"; if not (is_modifiable_lvalue env b1) then - err "left-hand side of assignment is not a modifiable l-value"; + err "expression is not assignable"; if not (wrap2 valid_assignment loc env b2 b1.etyp) then begin if wrap2 valid_cast loc env b2.etyp b1.etyp then - warning "assigning a value of type@ %a@ to a lvalue of type@ %a" - Cprint.typ b2.etyp Cprint.typ b1.etyp + if wrap2 int_pointer_conversion loc env b2.etyp b1.etyp then + warning Int_conversion + "incompatible integer to pointer conversion assigning to %a from %a" + (print_typ env) b1.etyp (print_typ env) b2.etyp + else + warning Int_conversion + "incompatible pointer to integer conversion assgining to %a from %a" + (print_typ env) b1.etyp (print_typ env) b2.etyp else - err "assigning a value of type@ %a@ to a lvalue of type@ %a" - Cprint.typ b2.etyp Cprint.typ b1.etyp; + err "assigning to %a from incompatible type %a" + (print_typ env) b1.etyp (print_typ env) b2.etyp; end; { edesc = EBinop(Oassign, b1, b2, b1.etyp); etyp = b1.etyp },env @@ -1742,16 +1798,22 @@ let elab_expr loc env a = begin match elab env (BINARY(sop, a1, a2)) with | ({ edesc = EBinop(_, b1, b2, _); etyp = ty } as b),env -> if List.mem AConst (attributes_of_type env b1.etyp) then - err "left-hand side of assignment has 'const' type"; + err "read-only variable is not assignable"; if not (is_modifiable_lvalue env b1) then - err ("left-hand side of assignment is not a modifiable l-value"); + err "expression is not assignable"; if not (wrap2 valid_assignment loc env b b1.etyp) then begin if wrap2 valid_cast loc env ty b1.etyp then - warning "assigning a value of type@ %a@ to a lvalue of type@ %a" - Cprint.typ ty Cprint.typ b1.etyp + if wrap2 int_pointer_conversion loc env ty b1.etyp then + warning Int_conversion + "incompatible integer to pointer conversion assigning to %a from %a" + (print_typ env) b1.etyp (print_typ env) ty + else + warning Int_conversion + "incompatible pointer to integer conversion assgining to %a from %a" + (print_typ env) b1.etyp (print_typ env) ty else - err "assigning a value of type@ %a@ to a lvalue of type@ %a" - Cprint.typ ty Cprint.typ b1.etyp; + err "assigning to %a from incompatible type %a" + (print_typ env) b1.etyp (print_typ env) ty; end; { edesc = EBinop(top, b1, b2, ty); etyp = b1.etyp },env | _ -> assert false @@ -1766,45 +1828,32 @@ let elab_expr loc env a = (* Elaboration of pre- or post- increment/decrement *) and elab_pre_post_incr_decr op msg a1 = - let b1,env = elab env a1 in - if not (is_modifiable_lvalue env b1) then - err "the argument of %s is not a modifiable l-value" msg; - if not (is_scalar_type env b1.etyp) then - err "the argument of %s must be an arithmetic or pointer type" msg; - { edesc = EUnop(op, b1); etyp = b1.etyp },env + let b1,env = elab env a1 in + if not (is_modifiable_lvalue env b1) then + err "expression is not assignable"; + if not (is_scalar_type env b1.etyp) then + err "cannot %s value of type %a" msg (print_typ env) b1.etyp; + { edesc = EUnop(op, b1); etyp = b1.etyp },env (* Elaboration of binary operators over integers *) - and elab_binary_integer msg op a1 a2 = - let b1,env = elab env a1 in - if not (is_integer_type env b1.etyp) then - error "the first argument of '%s' is not an integer type" msg; - let b2,env = elab env a2 in - if not (is_integer_type env b2.etyp) then - error "the second argument of '%s' is not an integer type" msg; - let tyres = binary_conversion env b1.etyp b2.etyp in - { edesc = EBinop(op, b1, b2, tyres); etyp = tyres },env + and elab_binary_integer op a1 a2 = + let b1,env = elab env a1 in + let b2,env = elab env a2 in + if not ((is_integer_type env b1.etyp) && (is_integer_type env b2.etyp)) then + error "invalid operands to binary expression (%a and %a)" + (print_typ env) b1.etyp (print_typ env) b2.etyp; + let tyres = binary_conversion env b1.etyp b2.etyp in + { edesc = EBinop(op, b1, b2, tyres); etyp = tyres },env (* Elaboration of binary operators over arithmetic types *) - and elab_binary_arithmetic msg op a1 a2 = - let b1,env = elab env a1 in - if not (is_arith_type env b1.etyp) then - error "the first argument of '%s' is not an arithmetic type" msg; - let b2,env = elab env a2 in - if not (is_arith_type env b2.etyp) then - error "the second argument of '%s' is not an arithmetic type" msg; - let tyres = binary_conversion env b1.etyp b2.etyp in - { edesc = EBinop(op, b1, b2, tyres); etyp = tyres },env - -(* Elaboration of shift operators *) - and elab_shift msg op a1 a2 = - let b1,env = elab env a1 in - if not (is_integer_type env b1.etyp) then - error "the first argument of '%s' is not an integer type" msg; - let b2,env = elab env a2 in - if not (is_integer_type env b2.etyp) then - error "the second argument of '%s' is not an integer type" msg; - let tyres = unary_conversion env b1.etyp in - { edesc = EBinop(op, b1, b2, tyres); etyp = tyres },env + and elab_binary_arithmetic op a1 a2 = + let b1,env = elab env a1 in + let b2,env = elab env a2 in + if not ((is_arith_type env b1.etyp) && (is_arith_type env b2.etyp)) then + error "invalid operands to binary expression (%a and %a)" + (print_typ env) b1.etyp (print_typ env) b2.etyp; + let tyres = binary_conversion env b1.etyp b2.etyp in + { edesc = EBinop(op, b1, b2, tyres); etyp = tyres },env (* Elaboration of comparisons *) and elab_comparison op a1 a2 = @@ -1826,50 +1875,60 @@ let elab_expr loc env a = EBinop(op, b1, b2, TPtr(ty1, [])) | TPtr(ty1, _), TPtr(ty2, _) -> if not (compatible_types AttrIgnoreAll env ty1 ty2) then - warning "comparison between incompatible pointer types"; + warning Compare_distinct_pointer_types "comparison of distinct pointer types (%a and %a)" + (print_typ env) b1.etyp (print_typ env) b2.etyp; EBinop(op, b1, b2, TPtr(ty1, [])) | TPtr _, (TInt _ | TEnum _) | (TInt _ | TEnum _), TPtr _ -> - warning "comparison between integer and pointer"; + warning Unnamed "ordered comparison between pointer and integer (%a and %a)" + (print_typ env) b1.etyp (print_typ env) b2.etyp; EBinop(op, b1, b2, TPtr(TVoid [], [])) - | _, _ -> + | ty1, ty2 -> error "illegal comparison between types@ %a@ and %a" - Cprint.typ b1.etyp Cprint.typ b2.etyp in + (print_typ env) b1.etyp (print_typ env) b2.etyp; in { edesc = resdesc; etyp = TInt(IInt, []) },env (* Elaboration of && and || *) and elab_logical_operator msg op a1 a2 = - let b1,env = elab env a1 in - if not (is_scalar_type env b1.etyp) then - err "the first argument of '%s' is not a scalar type" msg; - let b2,env = elab env a2 in - if not (is_scalar_type env b2.etyp) then - err "the second argument of '%s' is not a scalar type" msg; - { edesc = EBinop(op, b1, b2, TInt(IInt, [])); etyp = TInt(IInt, []) },env + let b1,env = elab env a1 in + let b2,env = elab env a2 in + if not ((is_scalar_type env b1.etyp) && (is_scalar_type env b2.etyp)) then + error "invalid operands to binary expression (%a and %a)" + (print_typ env) b1.etyp (print_typ env) b2.etyp; + { edesc = EBinop(op, b1, b2, TInt(IInt, [])); etyp = TInt(IInt, []) },env (* Type-checking of function arguments *) and elab_arguments argno args params vararg = match args, params with | ([],env), [] -> [],env - | ([],env), _::_ -> err "not enough arguments in function call"; [], env - | (_::_,env), [] -> + | ([],env), _::_ -> + let found = argno - 1 in + let expected = List.length params + found in + err "too few arguments to function call, expected %d, have %d" expected found; [],env + | (_::_,env), [] -> if vararg then args - else (err "too many arguments in function call"; args) + else + let expected = argno - 1 in + let found = List.length (fst args) + expected in + (err "too many arguments to function call, expected %d, have %d" expected found; args) | (arg1 :: argl,env), (_, ty_p) :: paraml -> let ty_a = argument_conversion env arg1.etyp in if not (wrap2 valid_assignment loc env {arg1 with etyp = ty_a} ty_p) then begin - if wrap2 valid_cast loc env ty_a ty_p then - warning - "argument #%d of function call has type@ %a@ \ - instead of the expected type@ %a" - argno Cprint.typ ty_a Cprint.typ ty_p + if wrap2 valid_cast loc env ty_a ty_p then begin + if wrap2 int_pointer_conversion loc env ty_a ty_p then + warning Int_conversion + "incompatible integer to pointer conversion passing %a to parameter of type %a" + (print_typ env) ty_a (print_typ env) ty_p + else + warning Int_conversion + "incompatible pointer to integer conversion passing %a to parameter of type %a" + (print_typ env) ty_a (print_typ env) ty_p end else err - "argument #%d of function call has type@ %a@ \ - instead of the expected type@ %a" - argno Cprint.typ ty_a Cprint.typ ty_p + "passing %a to parameter of incompatible type %a" + (print_typ env) ty_a (print_typ env) ty_p end; let rest,env = elab_arguments (argno + 1) (argl,env) paraml vararg in arg1 :: rest,env @@ -1899,22 +1958,22 @@ let __func__type_and_init s = let enter_typedefs loc env sto dl = if sto <> Storage_default then - error loc "Non-default storage on 'typedef' definition"; + error loc "cannot combine with previous 'typedef' declaration specifier"; List.fold_left (fun env (s, ty, init) -> if init <> NO_INIT then error loc "initializer in typedef"; match previous_def Env.lookup_typedef env s with | Some (s',ty') -> - if equal_types env ty ty' then begin - warning loc "redefinition of typedef '%s'" s; + if equal_types env ty ty' then env - end else begin - error loc "redefinition of typedef '%s' with different type" s; + else begin + error loc "typdef redefinition with different types (%a vs %a)" + (print_typ env) ty (print_typ env) ty'; env end | None -> if redef Env.lookup_ident env s then - error loc "redefinition of identifier '%s' as different kind of symbol" s; + error loc "redefinition of '%s' as different kind of symbol" s; let (id, env') = Env.enter_typedef env s ty in emit_elab env loc (Gtypedef(id, ty)); env') env dl @@ -1922,15 +1981,19 @@ let enter_typedefs loc env sto dl = let enter_decdefs local loc env sto dl = (* Sanity checks on storage class *) if sto = Storage_register && not local then - fatal_error loc "'register' on global declaration"; + fatal_error loc "illegal storage class on file-scoped variable"; if sto <> Storage_default && dl = [] then - warning loc "Storage class specifier on empty declaration"; + warning loc Missing_declarations "declaration does not declare anything"; let enter_decdef (decls, env) (s, ty, init) = let isfun = is_function_type env ty in if sto = Storage_extern && init <> NO_INIT then - error loc "'extern' declaration cannot have an initializer"; - if local && isfun && (sto = Storage_static || sto = Storage_register) then - error loc "invalid storage class for '%s'" s; + error loc "'extern' declaration variable has an initializer"; + if local && isfun then begin + match sto with + | Storage_static -> error loc "function declared in block scope cannot have 'static' storage class"; + | Storage_register -> error loc "illegal storage class on function"; + | _ -> () + end; (* Local function declarations are always treated as extern *) let sto1 = if local && isfun then Storage_extern else sto in (* enter ident in environment with declared type, because @@ -1945,7 +2008,7 @@ let enter_decdefs local loc env sto dl = if local && sto' <> Storage_extern && not isfun && wrap incomplete_type loc env ty' then - error loc "'%s' has incomplete type" s; + error loc "variable has incomplete type %a" (print_typ env) ty'; if local && not isfun && sto' <> Storage_extern && sto' <> Storage_static then (* Local definition *) ((sto', id, ty', init') :: decls, env2) @@ -1978,14 +2041,14 @@ let elab_KR_function_parameters env params defs loc = (* Check that the parameters have unique names *) List.iter (fun id -> if List.length (List.filter ((=) id) params) > 1 then - error loc "Parameter '%s' appears more than once in function declaration" id) + fatal_error loc "redefinition of parameter '%s'" id) params; (* Check that the declarations only declare parameters *) let extract_name (Init_name(Name(s, dty, attrs, loc') as name, ie)) = if not (List.mem s params) then error loc' "Declaration of '%s' which is not a function parameter" s; if ie <> NO_INIT then - error loc' "Illegal initialization of function parameter '%s'" s; + error loc' "parameter '%s' is initialized" s; name in (* Extract names and types from the declarations *) @@ -1994,7 +2057,7 @@ let elab_KR_function_parameters env params defs loc = let name_list = List.map extract_name name_init_list in let (paramsenv, sto) = elab_name_group loc' env (spec', name_list) in if sto <> Storage_default && sto <> Storage_register then - error loc' "'extern' or 'static' storage not supported for function parameter"; + error loc' "invalid storage class specifier in function declarator"; paramsenv | d -> (* Should never be produced by the parser *) fatal_error (get_definitionloc d) @@ -2007,11 +2070,11 @@ let elab_KR_function_parameters env params defs loc = | [] -> (* Parameter is not declared, defaults to "int" in ISO C90, is an error in ISO C99. Just emit a warning. *) - warning loc "Type of '%s' defaults to 'int'" param; + warning loc Pedantic "type of '%s' defaults to 'int'" param; TInt (IInt, []) | (_, ty) :: rem -> if rem <> [] then - error loc "Parameter '%s' defined more than once" param; + error loc "redefinition of parameter '%s'" param; ty in (* Match parameters against declarations *) let rec match_params params' extra_decls = function @@ -2060,11 +2123,11 @@ let elab_fundef env spec name defs body loc = let (s, sto, inline, noret, ty, kr_params, env1) = elab_fundef_name env spec name in if sto = Storage_register then - fatal_error loc "A function definition cannot have 'register' storage class"; + fatal_error loc "illegal storage class on function"; begin match kr_params, defs with - | None, d :: _ -> - error (get_definitionloc d) - "Old-style parameter declaration in a new-style function definition" + | None, d::_ -> + error (get_definitionloc d) + "old-style parameter declarations in prototyped function definition" | _ -> () end; (* Process the parameters and the K&R declarations, if any, to obtain: @@ -2078,7 +2141,6 @@ let elab_fundef env spec name defs body loc = | ty, None -> (ty, []) | TFun(ty_ret, None, false, attr), Some params -> - warning loc "Non-prototype, pre-standard function definition.@ Converting to prototype form"; let (params', extra_decls) = elab_KR_function_parameters env params defs loc in (TFun(ty_ret, Some params', inherit_vararg env s sto ty, attr), extra_decls) @@ -2089,12 +2151,11 @@ let elab_fundef env spec name defs body loc = let (ty_ret, params, vararg, attr) = match ty with | TFun(ty_ret, Some params, vararg, attr) -> - if wrap incomplete_type loc env1 ty_ret - && not (is_void_type env ty_ret) - then error loc "return type is an incomplete type"; - (ty_ret, params, vararg, attr) - | _ -> - fatal_error loc "wrong type for function definition" in + if wrap incomplete_type loc env1 ty_ret && not (is_void_type env ty_ret) then + fatal_error loc "incomplete result type %a in function definition" + (print_typ env) ty_ret; + (ty_ret, params, vararg, attr) + | _ -> fatal_error loc "wrong type for function definition" in (* Enter function in the environment, for recursive references *) let (fun_id, sto1, env1, _, _) = enter_or_refine_ident false loc env1 s sto ty in @@ -2122,7 +2183,7 @@ let elab_fundef env spec name defs body loc = sseq no_loc body1 {sdesc = Sreturn(Some(intconst 0L IInt)); sloc = no_loc} | _ -> - warning loc "return type of 'main' should be 'int'"; + warning loc Main_return_type "return type of 'main' should be 'int'"; body1 end else body1 in (* Add the extra declarations if any *) @@ -2133,7 +2194,7 @@ let elab_fundef env spec name defs body loc = sloc = no_loc } end in if noret && contains_return body1 then - warning loc "function '%s' declared 'noreturn' should not return" s; + warning loc Invalid_noreturn "function '%s' declared 'noreturn' should not return" s; (* Build and emit function definition *) let fn = { fd_storage = sto1; @@ -2156,7 +2217,7 @@ let rec elab_definition (local: bool) (env: Env.t) (def: Cabs.definition) (* "int f(int x) { ... }" *) (* "int f(x, y) double y; { ... }" *) | FUNDEF(spec, name, defs, body, loc) -> - if local then error loc "local definition of a function"; + if local then error loc "function definition is not allowed here"; let env1 = elab_fundef env spec name defs body loc in ([], env1) @@ -2215,7 +2276,7 @@ let stmt_labels stmt = | DEFAULT(s1, _) -> do_stmt s1 | LABEL(lbl, s1, loc) -> if StringSet.mem lbl !lbls then - error loc "multiply-defined label '%s'\n" lbl; + error loc "redefinition of label '%s'\n" lbl; lbls := StringSet.add lbl !lbls; do_stmt s1 | _ -> () @@ -2248,7 +2309,7 @@ let rec elab_stmt env ctx s = let a',env = elab_expr loc env a in begin match Ceval.integer_expr env a' with | None -> - error loc "argument of 'case' must be an integer compile-time constant" + error loc "expression is not an integer constant expression" | Some n -> () end; let s1,env = elab_stmt env ctx s1 in @@ -2268,7 +2329,8 @@ let rec elab_stmt env ctx s = | If(a, s1, s2, loc) -> let a',env = elab_expr loc env a in if not (is_scalar_type env a'.etyp) then - error loc "the condition of 'if' does not have scalar type"; + error loc "statement requires expression of scalar type (%a invalid)" + (print_typ env) a'.etyp; let s1',env = elab_stmt env ctx s1 in let s2',env = match s2 with @@ -2282,7 +2344,8 @@ let rec elab_stmt env ctx s = | WHILE(a, s1, loc) -> let a',env = elab_expr loc env a in if not (is_scalar_type env a'.etyp) then - error loc "the condition of 'while' does not have scalar type"; + error loc "statement requires expression of scalar type (%a invalid)" + (print_typ env) a'.etyp; let s1',env = elab_stmt env (ctx_loop ctx) s1 in { sdesc = Swhile(a', s1'); sloc = elab_loc loc },env @@ -2290,7 +2353,8 @@ let rec elab_stmt env ctx s = let s1',env = elab_stmt env (ctx_loop ctx) s1 in let a',env = elab_expr loc env a in if not (is_scalar_type env a'.etyp) then - error loc "the condition of 'while' does not have scalar type"; + error loc "statement requires expression of scalar type (%a invalid)" + (print_typ env) a'.etyp; { sdesc = Sdowhile(s1', a'); sloc = elab_loc loc },env | FOR(fc, a2, a3, s1, loc) -> @@ -2313,7 +2377,7 @@ let rec elab_stmt env ctx s = | Some a2 -> elab_expr loc env' a2 in if not (is_scalar_type env' a2'.etyp) then - error loc "the condition of 'for' does not have scalar type"; + error loc "statement requires expression of scalar type (%a invalid)" (print_typ env) a2'.etyp; let a3',env' = elab_for_expr loc env' a3 in let s1',env' = elab_stmt env' (ctx_loop ctx) s1 in let sfor = { sdesc = Sfor(a1', a2', a3', s1'); sloc = elab_loc loc } in @@ -2326,18 +2390,19 @@ let rec elab_stmt env ctx s = | SWITCH(a, s1, loc) -> let a',env = elab_expr loc env a in if not (is_integer_type env a'.etyp) then - error loc "the argument of 'switch' is not an integer"; + error loc "statement requires expression of integer type (%a invalid)" + (print_typ env) a'.etyp; let s1',env = elab_stmt env (ctx_switch ctx) s1 in { sdesc = Sswitch(a', s1'); sloc = elab_loc loc },env (* 6.8.6 Break and continue statements *) | BREAK loc -> if not ctx.ctx_break then - error loc "'break' outside of a loop or a 'switch'"; + error loc "'break' statement not in loop or switch statement"; { sdesc = Sbreak; sloc = elab_loc loc },env | CONTINUE loc -> if not ctx.ctx_continue then - error loc "'continue' outside of a loop"; + error loc "'continue' statement not in loop statement"; { sdesc = Scontinue; sloc = elab_loc loc },env (* 6.8.6 Return statements *) @@ -2347,24 +2412,26 @@ let rec elab_stmt env ctx s = | TVoid _, None -> () | TVoid _, Some _ -> error loc - "'return' with a value in a function of return type 'void'" + "'return' with a value in a function returning void" | _, None -> - warning loc - "'return' without a value in a function of return type@ %a" - Cprint.typ ctx.ctx_return_typ + warning loc Return_type + "'return' with no value, in a function returning non-void" | _, Some b -> if not (wrap2 valid_assignment loc env b ctx.ctx_return_typ) then begin if wrap2 valid_cast loc env b.etyp ctx.ctx_return_typ then - warning loc - "return value has type@ %a@ \ - instead of the expected type@ %a" - Cprint.typ b.etyp Cprint.typ ctx.ctx_return_typ + if wrap2 int_pointer_conversion loc env b.etyp ctx.ctx_return_typ then + warning loc Int_conversion + "incompatible integer to pointer conversion returning %a from a function with result type %a" + (print_typ env) b.etyp (print_typ env) ctx.ctx_return_typ + else + warning loc Int_conversion + "incompatible integer to pointer conversion returning %a from a function with result type %a" + (print_typ env) b.etyp (print_typ env) ctx.ctx_return_typ else error loc - "return value has type@ %a@ \ - instead of the expected type@ %a" - Cprint.typ b.etyp Cprint.typ ctx.ctx_return_typ + "returning %a from a function with incompatible result type %a" + (print_typ env) b.etyp (print_typ env) ctx.ctx_return_typ end end; { sdesc = Sreturn a'; sloc = elab_loc loc },env @@ -2372,7 +2439,7 @@ let rec elab_stmt env ctx s = (* 6.8.6 Goto statements *) | GOTO(lbl, loc) -> if not (StringSet.mem lbl ctx.ctx_labels) then - error loc "unknown 'goto' label %s" lbl; + error loc "use of undeclared label '%s'" lbl; { sdesc = Sgoto lbl; sloc = elab_loc loc },env (* 6.8.3 Null statements *) diff --git a/cparser/Env.ml b/cparser/Env.ml index dae79ef2..cbfafd48 100644 --- a/cparser/Env.ml +++ b/cparser/Env.ml @@ -260,17 +260,17 @@ let composite_tag_name name = let error_message = function | Unbound_identifier name -> - sprintf "Unbound identifier '%s'" name + sprintf "use of undeclared identifier '%s'" name | Unbound_tag(name, kind) -> - sprintf "Unbound %s '%s'" kind (composite_tag_name name) + sprintf "unbound %s '%s'" kind (composite_tag_name name) | Tag_mismatch(name, expected, actual) -> sprintf "'%s' was declared as a %s but is used as a %s" (composite_tag_name name) actual expected | Unbound_typedef name -> - sprintf "Unbound typedef '%s'" name + sprintf "unbound typedef '%s'" name | No_member(compname, compkind, memname) -> - sprintf "%s '%s' has no member named '%s'" - compkind (composite_tag_name compname) memname + sprintf "no member named '%s' in '%s %s'" + memname compkind (composite_tag_name compname) let _ = Printexc.register_printer diff --git a/cparser/ExtendedAsm.ml b/cparser/ExtendedAsm.ml index fc228aca..30d1a0cc 100644 --- a/cparser/ExtendedAsm.ml +++ b/cparser/ExtendedAsm.ml @@ -104,14 +104,14 @@ let rec transf_inputs loc env accu pos pos' subst = function let n = match Ceval.integer_expr env e with | Some n -> n - | None -> error "%aError: asm argument of kind '%s' is not a constant" - formatloc loc cstr; + | None -> error loc "asm argument of kind '%s' is not a constant" + cstr; 0L in transf_inputs loc env accu (pos + 1) pos' (set_label_const lbl pos n subst) inputs end else begin - error "%aUnsupported feature: asm argument of kind '%s'" - formatloc loc cstr; + error loc "unsupported feature: asm argument of kind '%s'" + cstr; transf_inputs loc env (e :: accu) (pos + 1) (pos' + 1) (set_label_reg lbl pos pos' subst) inputs end @@ -127,7 +127,7 @@ let transf_outputs loc env = function (None, [], StringMap.empty, 0, 0) | [(lbl, cstr, e)] -> if not (is_modifiable_lvalue env e) then - error "%aError: asm output is not a modifiable l-value" formatloc loc; + error loc "asm output is not a modifiable l-value"; let valid = Str.string_match re_valid_output cstr 0 in if valid && String.contains cstr 'r' then if is_reg_pair env e.etyp then @@ -139,13 +139,12 @@ let transf_outputs loc env = function (None, [eaddrof e], set_label_mem lbl 0 0 StringMap.empty, 1, 1) else begin - error "%aUnsupported feature: asm result of kind '%s'" - formatloc loc cstr; + error loc "unsupported feature: asm result of kind '%s'" + cstr; (None, [], set_label_reg lbl 0 0 StringMap.empty, 1, 1) end | outputs -> - error "%aUnsupported feature: asm statement with 2 or more outputs" - formatloc loc; + error loc "unsupported feature: asm statement with 2 or more outputs"; (* Bind the outputs so that we don't get another error when substituting the text *) let rec bind_outputs pos subst = function @@ -163,8 +162,7 @@ let check_clobbers loc clob = || Machregsaux.is_scratch_register c || c = "memory" || c = "cc" (* GCC does not accept MEMORY or CC *) then () - else error "%aError: unrecognized asm register clobber '%s'" - formatloc loc c) + else error loc "unrecognized asm register clobber '%s'" c) clob (* Renaming of the %nnn and %[ident] placeholders in the asm text *) @@ -178,8 +176,7 @@ let rename_placeholders loc template subst = try StringMap.find p subst with Not_found -> - error "%aError: '%s' in asm text does not designate any operand" - formatloc loc p; + error loc"'%s' in asm text does not designate any operand" p; "%" in Str.global_substitute re_asm_placeholder diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll index d3747e22..71aad604 100644 --- a/cparser/Lexer.mll +++ b/cparser/Lexer.mll @@ -126,16 +126,16 @@ let currentLoc = (* Error reporting *) let fatal_error lb fmt = - Cerrors.fatal_error ("%s:%d: Error:@ " ^^ fmt) - lb.lex_curr_p.pos_fname lb.lex_curr_p.pos_lnum + Cerrors.fatal_error + (lb.lex_curr_p.pos_fname,lb.lex_curr_p.pos_lnum) fmt let error lb fmt = - Cerrors.error ("%s:%d: Error:@ " ^^ fmt) - lb.lex_curr_p.pos_fname lb.lex_curr_p.pos_lnum + Cerrors.error + (lb.lex_curr_p.pos_fname,lb.lex_curr_p.pos_lnum) fmt let warning lb fmt = - Cerrors.warning ("%s:%d: Warning:@ " ^^ fmt) - lb.lex_curr_p.pos_fname lb.lex_curr_p.pos_lnum + Cerrors.warning + (lb.lex_curr_p.pos_fname,lb.lex_curr_p.pos_lnum) Cerrors.Unnamed ("warning: " ^^ fmt) (* Simple character escapes *) diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml index aafa1caa..a921e2d8 100644 --- a/cparser/PackedStructs.ml +++ b/cparser/PackedStructs.ml @@ -48,7 +48,7 @@ let safe_alignof loc env ty = match alignof env ty with | Some al -> al | None -> - error "%aError: incomplete type for a struct field" formatloc loc; 1 + error loc "incomplete type for a struct field"; 1 (* Remove existing [_Alignas] attributes and add the given [_Alignas] attr. *) @@ -61,14 +61,13 @@ let set_alignas_attr al attrs = let transf_field_decl mfa swapped loc env struct_id f = if f.fld_bitfield <> None then - error "%aError: bitfields in packed structs not allowed" - formatloc loc; + error loc "bitfields in packed structs not allowed"; (* Register as byte-swapped if needed *) if swapped then begin let (can_swap, must_swap) = can_byte_swap env f.fld_typ in if not can_swap then - error "%aError: cannot byte-swap field of type '%a'" - formatloc loc Cprint.typ f.fld_typ; + error loc "cannot byte-swap field of type '%a'" + Cprint.typ f.fld_typ; if must_swap then Hashtbl.add byteswapped_fields (struct_id, f.fld_name) () end; @@ -99,11 +98,11 @@ let is_pow2 n = n > 0 && n land (n - 1) = 0 let packed_param_value loc n = let m = Int64.to_int n in if n <> Int64.of_int m then - (error "%a: __packed__ parameter `%Ld' is too large" formatloc loc n; 0) + (error loc "__packed__ parameter `%Ld' is too large" n; 0) else if m = 0 || is_pow2 m then m else - (error "%a: __packed__ parameter `%Ld' must be a power of 2" formatloc loc n; 0) + (error loc "__packed__ parameter `%Ld' must be a power of 2" n; 0) let transf_composite loc env su id attrs ml = match su with @@ -117,8 +116,7 @@ let transf_composite loc env su id attrs ml = | [[AInt n; AInt p]] -> (n, p, false) | [[AInt n; AInt p; AInt q]] -> (n, p, q <> 0L) | _ -> - error "%a: ill-formed or ambiguous __packed__ attribute" - formatloc loc; + error loc "ill-formed or ambiguous __packed__ attribute"; (0L, 0L, false) in let mfa = packed_param_value loc mfa in let msa = packed_param_value loc msa in @@ -140,7 +138,7 @@ let accessor_type loc env ty = | TEnum(_,_) -> (8 * sizeof_ikind enum_ikind, TInt(unsigned_ikind_of enum_ikind,[])) | TPtr _ -> (8 * !config.sizeof_ptr, TInt(ptr_t_ikind(),[])) | _ -> - error "%a: unsupported type for byte-swapped field access" formatloc loc; + error loc "unsupported type for byte-swapped field access"; (32, TVoid []) (* (ty) e *) @@ -175,7 +173,7 @@ let bswap_read loc env lval = ecast_opt env ty call end with Env.Error msg -> - fatal_error "%aError: %s" formatloc loc (Env.error_message msg) + fatal_error loc "%s" (Env.error_message msg) (* __builtin_write_intNN_reversed(&lhs,rhs) or lhs = __builtin_bswapNN(rhs) *) @@ -202,7 +200,7 @@ let bswap_write loc env lhs rhs = eassign lhs (ecast_opt env ty call) end with Env.Error msg -> - fatal_error "%aError: %s" formatloc loc (Env.error_message msg) + fatal_error loc "%s" (Env.error_message msg) (* Expressions *) @@ -248,7 +246,7 @@ let transf_expr loc env ctx e = | EUnop(Oaddrof, e1) -> let (e1', swap) = lvalue e1 in if swap then - error "%aError: & over byte-swapped field" formatloc loc; + error loc "& over byte-swapped field"; {edesc = EUnop(Oaddrof, e1'); etyp = e.etyp} | EUnop((Opreincr|Opredecr) as op, e1) -> @@ -349,8 +347,8 @@ let transf_init loc env i = let n' = byteswap_int (sizeof_ikind ik) n in Init_single {edesc = EConst(CInt(n', ik, "")); etyp = e.etyp} | _ -> - error "%aError: initializer for byte-swapped field is not \ - a compile-time integer constant" formatloc loc; i + error loc "initializer for byte-swapped field is not \ + a compile-time integer constant"; i end | Init_array il -> let swap_elt = diff --git a/cparser/Parse.ml b/cparser/Parse.ml index c125e653..ebe62621 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -70,7 +70,7 @@ let preprocessed_file transfs name sourcefile = | Parser.Parser.Inter.Fail_pr -> (* Theoretically impossible : implies inconsistencies between grammars. *) - Cerrors.fatal_error "Internal error while parsing" + Cerrors.fatal_error Cutil.no_loc "Internal error while parsing" | Parser.Parser.Inter.Timeout_pr -> assert false | Parser.Parser.Inter.Parsed_pr (ast, _ ) -> ast) in let p1 = Timing.time "Elaboration" Elab.elab_file ast in diff --git a/cparser/Rename.ml b/cparser/Rename.ml index 664f6a28..c62c6763 100644 --- a/cparser/Rename.ml +++ b/cparser/Rename.ml @@ -94,7 +94,7 @@ let ident env id = try IdentMap.find id env.re_id with Not_found -> - Cerrors.fatal_error "Internal error: Rename: %s__%d unbound" + Cerrors.fatal_error no_loc "internal error: rename: %s__%d unbound" id.name id.stamp let rec typ env = function @@ -292,4 +292,3 @@ let program p file = globdecls (reserve_public (reserve_builtins()) file p) [] p - diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml index 0669be6e..87b2f9bb 100644 --- a/cparser/Unblock.ml +++ b/cparser/Unblock.ml @@ -32,7 +32,7 @@ let rec local_initializer env path init k = let (ty_elt, sz) = match unroll env path.etyp with | TArray(ty_elt, Some sz, _) -> (ty_elt, sz) - | _ -> fatal_error "Wrong type for array initializer" in + | _ -> fatal_error no_loc "Wrong type for array initializer" in let rec array_init pos il = if pos >= sz then k else begin let (i1, il') = diff --git a/driver/Driver.ml b/driver/Driver.ml index a0ec07f1..038bd423 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -339,8 +339,9 @@ General options:\n\ \ -stdlib Set the path of the Compcert run-time library\n\ \ -v Print external commands before invoking them\n\ \ -timings Show the time spent in various compiler passes\n\ -\ -version Print the version string and exit\n\ -Interpreter mode:\n\ +\ -version Print the version string and exit\n" ^ + Cerrors.warning_help ^ +"Interpreter mode:\n\ \ -interp Execute given .c files using the reference interpreter\n\ \ -quiet Suppress diagnostic messages for the interpreter\n\ \ -trace Have the interpreter produce a detailed trace of reductions\n\ @@ -446,10 +447,11 @@ let cmdline_actions = (* General options *) Exact "-v", Set option_v; Exact "-stdlib", String(fun s -> stdlib_path := s); - Exact "-timings", Set option_timings; - Exact "-Werror", Set Cerrors.warn_error; + Exact "-timings", Set option_timings;] @ +(* Diagnostic options *) + Cerrors.warning_options @ (* Interpreter mode *) - Exact "-interp", Set option_interp; + [ Exact "-interp", Set option_interp; Exact "-quiet", Self (fun _ -> Interp.trace := 0); Exact "-trace", Self (fun _ -> Interp.trace := 2); Exact "-random", Self (fun _ -> Interp.mode := Interp.Random); -- cgit From 8a740c6d441afd980e3bdb43d1844bd23e0ad55b Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 5 Aug 2016 17:48:53 +0200 Subject: Additional test for color output. Color output is only enabled if stderr is a tty, and the environment variable TERM is not empty or dumb. Bug 18004 --- cparser/Cerrors.ml | 35 ++++++++++++-------------- cparser/Cerrors.mli | 63 ++++++++++++++++++++++++++++++++--------------- driver/Commandline.ml | 4 +++ driver/Commandline.mli | 2 ++ driver/Driver.ml | 53 ++++++++++++++++++++------------------- exportclight/Clightgen.ml | 20 +++++++-------- 6 files changed, 102 insertions(+), 75 deletions(-) diff --git a/cparser/Cerrors.ml b/cparser/Cerrors.ml index f2794a2c..8ee13caf 100644 --- a/cparser/Cerrors.ml +++ b/cparser/Cerrors.ml @@ -18,9 +18,10 @@ open Format open Commandline -let warn_error = ref false let error_fatal = ref false -let color_diagnostics = ref true +let color_diagnostics = + let term = try Sys.getenv "TERM" with Not_found -> "" in + ref (Unix.isatty Unix.stderr && term <> "dumb" && term <>"") let num_errors = ref 0 let num_warnings = ref 0 @@ -106,20 +107,20 @@ let string_of_warning = function | Literal_range -> "literal-range" | Unknown_pragmas -> "unknown-pragmas" -let activate_warning w = +let activate_warning w () = if not (List.mem w !active_warnings) then active_warnings:=w::!active_warnings -let deactivate_warning w = +let deactivate_warning w () = active_warnings:=List.filter ((<>) w) !active_warnings; error_warnings:= List.filter ((<>) w) !error_warnings -let warning_as_error w = - activate_warning w; +let warning_as_error w ()= + activate_warning w (); if not (List.mem w !error_warnings) then error_warnings := w::!error_warnings -let warning_not_as_error w = +let warning_not_as_error w () = error_warnings:= List.filter ((<>) w) !error_warnings let wall () = @@ -256,18 +257,14 @@ let check_errors () = eprintf "@[%d error%s detected.@]@." !num_errors (if !num_errors = 1 then "" else "s"); - if !warn_error && !num_warnings > 0 then - eprintf "@[%d error-enabled warning%s detected.@]@." - !num_warnings - (if !num_warnings = 1 then "" else "s"); - !num_errors > 0 || (!warn_error && !num_warnings > 0) + !num_errors > 0 let error_option w = let key = string_of_warning w in - [Exact ("-W"^key), Self (fun _ -> activate_warning w); - Exact ("-Wno"^key), Self (fun _ -> deactivate_warning w); - Exact ("-Werror="^key), Self (fun _ -> warning_as_error w); - Exact ("-Wno-error="^key), Self (fun _ -> warning_not_as_error w)] + [Exact ("-W"^key), Unit (activate_warning w); + Exact ("-Wno"^key), Unit (deactivate_warning w); + Exact ("-Werror="^key), Unit ( warning_as_error w); + Exact ("-Wno-error="^key), Unit ( warning_not_as_error w)] let warning_options = error_option Unnamed @ @@ -289,10 +286,10 @@ let warning_options = error_option Literal_range @ error_option Unknown_pragmas @ [Exact ("-Wfatal-errors"), Set error_fatal; - Exact ("-fdiagnostics-color"), Set color_diagnostics; + Exact ("-fdiagnostics-color"), Ignore; (* Either output supports it or no color *) Exact ("-fno-diagnostics-color"), Unset color_diagnostics; - Exact ("-Werror"), Self (fun _ -> werror ()); - Exact ("-Wall"), Self (fun _ -> wall());] + Exact ("-Werror"), Unit werror; + Exact ("-Wall"), Unit wall;] let warning_help = "Diagnostic options:\n\ \ -W Enable the specific \n\ diff --git a/cparser/Cerrors.mli b/cparser/Cerrors.mli index 3010241a..b312931a 100644 --- a/cparser/Cerrors.mli +++ b/cparser/Cerrors.mli @@ -13,35 +13,58 @@ (* *) (* *********************************************************************) -val warn_error : bool ref +(* Printing of warnings and error messages *) + val reset : unit -> unit + (** Reset the error counters. *) + exception Abort -val fatal_error_raw : ('a, out_channel, unit, 'b) format4 -> 'a + (** Exception raised upon fatal errors *) + val check_errors : unit -> bool + (** Check whether errors occured *) type warning_type = - | Unnamed - | Unknown_attribute - | Zero_length_array - | Celeven_extension - | Gnu_empty_struct - | Missing_declarations - | Constant_conversion - | Int_conversion - | Varargs - | Implicit_function_declaration - | Pointer_type_mismatch - | Compare_distinct_pointer_types - | Pedantic - | Main_return_type - | Invalid_noreturn - | Return_type - | Literal_range - | Unknown_pragmas + | Unnamed (** warnings which cannot be turned off *) + | Unknown_attribute (** usage of unsupported/unknown attributes *) + | Zero_length_array (** gnu extension for zero lenght arrays *) + | Celeven_extension (** C11 fetatures *) + | Gnu_empty_struct (** gnu extension for empty struct *) + | Missing_declarations (** declation which do not declare anything *) + | Constant_conversion (** dangerous constant conversions *) + | Int_conversion (** pointer <-> int conversions *) + | Varargs (** promotable vararg argument *) + | Implicit_function_declaration (** deprecated implicit function declaration *) + | Pointer_type_mismatch (** pointer type mismatch in ?: operator *) + | Compare_distinct_pointer_types (** comparison between different pointer types *) + | Pedantic (** non C99 code *) + | Main_return_type (** wrong return type for main *) + | Invalid_noreturn (** noreturn function containing return *) + | Return_type (** void return in non-void function *) + | Literal_range (** literal ranges *) + | Unknown_pragmas (** unknown/unsupported pragma *) val warning : (string * int) -> warning_type -> ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a +(** [warning (f,c) w fmt arg1 ... argN] formats the arguments [arg1] to [argN] as warining according to + the format string [fmt] and outputs the result on [stderr] with additional file [f] and column [c] + and warning key for [w] *) + val error : (string * int) -> ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a +(** [error (f,c) w fmt arg1 ... argN] formats the arguments [arg1] to [argN] as error according to + the format string [fmt] and outputs the result on [stderr] with additional file [f] and column [c] + and warning key for [w]. *) + val fatal_error : (string * int) -> ('a, Format.formatter, unit, unit, unit, 'b) format6 -> 'a +(** [fatal_error (f,c) w fmt arg1 ... argN] formats the arguments [arg1] to [argN] as error according to + the format string [fmt] and outputs the result on [stderr] with additional file [f] and column [c] + and warning key for [w]. Additionally raises the excpetion [Abort] after printing the error message *) + +val fatal_error_raw : ('a, out_channel, unit, 'b) format4 -> 'a +(** [fatal_error_raw] is identical to fatal_error, except it uses [Printf] and does not automatically + introduce indentation *) val warning_help : string +(** Help string for all warning options *) + val warning_options : (Commandline.pattern * Commandline.action) list +(** List of all options for diagnostics *) diff --git a/driver/Commandline.ml b/driver/Commandline.ml index 0a2c8fca..c5c2b82c 100644 --- a/driver/Commandline.ml +++ b/driver/Commandline.ml @@ -31,6 +31,8 @@ type action = | Self of (string -> unit) | String of (string -> unit) | Integer of (int -> unit) + | Ignore + | Unit of (unit -> unit) let match_pattern text = function | Exact s -> @@ -95,6 +97,8 @@ let parse_array spec argv first last = end else begin eprintf "Option `%s' expects an argument\n" s; exit 2 end + | Some (Ignore) -> parse (i+1) + | Some (Unit f) -> f (); parse (i+1) end in parse first diff --git a/driver/Commandline.mli b/driver/Commandline.mli index 79786678..5f9d8704 100644 --- a/driver/Commandline.mli +++ b/driver/Commandline.mli @@ -33,6 +33,8 @@ type action = | Self of (string -> unit) (** call the function with the matched string *) | String of (string -> unit) (** read next arg as a string, call function *) | Integer of (int -> unit) (** read next arg as an int, call function *) + | Ignore (** ignore the arg *) + | Unit of (unit -> unit) (** call the function with unit as argument *) val parse_cmdline: (pattern * action) list -> unit diff --git a/driver/Driver.ml b/driver/Driver.ml index 038bd423..78baed47 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -348,10 +348,10 @@ General options:\n\ \ -random Randomize execution order\n\ \ -all Simulate all possible execution orders\n" -let print_usage_and_exit _ = +let print_usage_and_exit () = printf "%s" usage_string; exit 0 -let print_version_and_exit _ = +let print_version_and_exit () = printf "%s" version_string; exit 0 let language_support_options = [ @@ -364,8 +364,8 @@ let optimization_options = [ option_ftailcalls; option_fconstprop; option_fcse; option_fredundancy ] -let set_all opts = List.iter (fun r -> r := true) opts -let unset_all opts = List.iter (fun r -> r := false) opts +let set_all opts () = List.iter (fun r -> r := true) opts +let unset_all opts () = List.iter (fun r -> r := false) opts let num_source_files = ref 0 @@ -374,13 +374,16 @@ let num_input_files = ref 0 let cmdline_actions = let f_opt name ref = [Exact("-f" ^ name), Set ref; Exact("-fno-" ^ name), Unset ref] in + let dwarf_version version () = + option_g:=true; + option_gdwarf := version in [ (* Getting help *) - Exact "-help", Self print_usage_and_exit; - Exact "--help", Self print_usage_and_exit; + Exact "-help", Unit print_usage_and_exit; + Exact "--help", Unit print_usage_and_exit; (* Getting version info *) - Exact "-version", Self print_version_and_exit; - Exact "--version", Self print_version_and_exit; + Exact "-version", Unit print_version_and_exit; + Exact "--version", Unit print_version_and_exit; (* Processing options *) Exact "-c", Set option_c; Exact "-E", Set option_E; @@ -391,17 +394,15 @@ let cmdline_actions = (* Preprocessing options *) @ prepro_actions @ (* Language support options -- more below *) - [ Exact "-fall", Self (fun _ -> set_all language_support_options); - Exact "-fnone", Self (fun _ -> unset_all language_support_options); + [ Exact "-fall", Unit (set_all language_support_options); + Exact "-fnone", Unit (unset_all language_support_options); (* Debugging options *) - Exact "-g", Self (fun s -> option_g := true; - option_gdwarf := 3);] @ + Exact "-g", Unit (dwarf_version 3);] @ (if gnu_system then - [ Exact "-gdwarf-2", Self (fun s -> option_g:=true; - option_gdwarf := 2); - Exact "-gdwarf-3", Self (fun s -> option_g := true; - option_gdwarf := 3);] else []) @ - [ Exact "-frename-static", Self (fun s -> option_rename_static:= true); + [ Exact "-gdwarf-2", Unit (dwarf_version 2); + Exact "-gdwarf-3", Unit (dwarf_version 3);] + else []) @ + [ Exact "-frename-static", Set option_rename_static; Exact "-gdepth", Integer (fun n -> if n = 0 || n <0 then begin option_g := false end else begin @@ -409,9 +410,9 @@ let cmdline_actions = option_gdepth := if n > 3 then 3 else n end); (* Code generation options -- more below *) - Exact "-O0", Self (fun _ -> unset_all optimization_options); - Exact "-O", Self (fun _ -> set_all optimization_options); - _Regexp "-O[123]$", Self (fun _ -> set_all optimization_options); + Exact "-O0", Unit (unset_all optimization_options); + Exact "-O", Unit (set_all optimization_options); + _Regexp "-O[123]$", Unit (set_all optimization_options); Exact "-Os", Set option_Osize; Exact "-fsmall-data", Integer(fun n -> option_small_data := n); Exact "-fsmall-const", Integer(fun n -> option_small_const := n); @@ -420,8 +421,8 @@ let cmdline_actions = Exact "-falign-branch-targets", Integer(fun n -> option_falignbranchtargets := n); Exact "-falign-cond-branches", Integer(fun n -> option_faligncondbranchs := n); (* Target processor options *) - Exact "-conf", String (fun _ -> ()); (* Ignore option since it is already handled *) - Exact "-target", String (fun _ -> ());] @ (* Ignore option since it is already handled *) + Exact "-conf", Ignore; (* Ignore option since it is already handled *) + Exact "-target", Ignore;] @ (* Ignore option since it is already handled *) (if Configuration.arch = "arm" then [ Exact "-mthumb", Set option_mthumb; Exact "-marm", Unset option_mthumb; ] @@ -452,10 +453,10 @@ let cmdline_actions = Cerrors.warning_options @ (* Interpreter mode *) [ Exact "-interp", Set option_interp; - Exact "-quiet", Self (fun _ -> Interp.trace := 0); - Exact "-trace", Self (fun _ -> Interp.trace := 2); - Exact "-random", Self (fun _ -> Interp.mode := Interp.Random); - Exact "-all", Self (fun _ -> Interp.mode := Interp.All) + Exact "-quiet", Unit (fun () -> Interp.trace := 0); + Exact "-trace", Unit (fun () -> Interp.trace := 2); + Exact "-random", Unit (fun () -> Interp.mode := Interp.Random); + Exact "-all", Unit (fun () -> Interp.mode := Interp.All) ] (* -f options: come in -f and -fno- variants *) (* Language support options *) diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml index 0a586acd..bdbf8be9 100644 --- a/exportclight/Clightgen.ml +++ b/exportclight/Clightgen.ml @@ -98,10 +98,10 @@ Tracing options:\n\ General options:\n\ \ -v Print external commands before invoking them\n" -let print_usage_and_exit _ = +let print_usage_and_exit () = printf "%s" usage_string; exit 0 -let print_version_and_exit _ = +let print_version_and_exit () = printf "%s" version_string; exit 0 let language_support_options = [ @@ -110,26 +110,26 @@ let language_support_options = [ option_fpacked_structs; option_finline_asm ] -let set_all opts = List.iter (fun r -> r := true) opts -let unset_all opts = List.iter (fun r -> r := false) opts +let set_all opts () = List.iter (fun r -> r := true) opts +let unset_all opts () = List.iter (fun r -> r := false) opts let cmdline_actions = let f_opt name ref = [Exact("-f" ^ name), Set ref; Exact("-fno-" ^ name), Unset ref] in [ (* Getting help *) - Exact "-help", Self print_usage_and_exit; - Exact "--help", Self print_usage_and_exit; + Exact "-help", Unit print_usage_and_exit; + Exact "--help", Unit print_usage_and_exit; (* Getting version info *) - Exact "-version", Self print_version_and_exit; - Exact "--version", Self print_version_and_exit; + Exact "-version", Unit print_version_and_exit; + Exact "--version", Unit print_version_and_exit; (* Processing options *) Exact "-E", Set option_E;] (* Preprocessing options *) @ prepro_actions @ (* Language support options -- more below *) - [Exact "-fall", Self (fun _ -> set_all language_support_options); - Exact "-fnone", Self (fun _ -> unset_all language_support_options); + [Exact "-fall", Unit (set_all language_support_options); + Exact "-fnone", Unit (unset_all language_support_options); (* Tracing options *) Exact "-dparse", Set option_dparse; Exact "-dc", Set option_dcmedium; -- cgit From 3208e22ea89c459a5a7944ad8e82511d4a5328fa Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 16 Aug 2016 16:17:20 +0200 Subject: Added raw printing of types without formatting. This avoids introducing line breaks during printing of function types. Bug 18004 --- cparser/Cprint.ml | 11 ++++++++--- cparser/Cprint.mli | 1 + cparser/Elab.ml | 4 ++-- 3 files changed, 11 insertions(+), 5 deletions(-) diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml index e80a4c8e..2a110104 100644 --- a/cparser/Cprint.ml +++ b/cparser/Cprint.ml @@ -126,7 +126,7 @@ let name_of_fkind = function | FDouble -> "double" | FLongDouble -> "long double" -let rec dcl pp ty n = +let rec dcl ?(pp_indication=true) pp ty n = match ty with | TVoid a -> fprintf pp "void%a%t" attributes a n @@ -160,7 +160,8 @@ let rec dcl pp ty n = | [] -> n pp | _ -> fprintf pp " (%a%t)" attributes a n end; - fprintf pp "(@["; + fprintf pp "("; + if pp_indication then fprintf pp "@["; begin match args with | None -> () | Some [] -> if vararg then fprintf pp "..." else fprintf pp "void" @@ -169,7 +170,8 @@ let rec dcl pp ty n = List.iter (fun a -> fprintf pp ",@ "; param a) al; if vararg then fprintf pp ",@ ..." end; - fprintf pp "@])" in + if pp_indication then fprintf pp "@]"; + fprintf pp ")" in dcl pp tres n' | TNamed(id, a) -> fprintf pp "%a%a%t" ident id attributes a n @@ -183,6 +185,9 @@ let rec dcl pp ty n = let typ pp ty = dcl pp ty (fun _ -> ()) +let typ_raw pp ty = + dcl ~pp_indication:false pp ty (fun _ -> ()) + type associativity = LtoR | RtoL | NA let precedence = function (* H&S section 7.2 *) diff --git a/cparser/Cprint.mli b/cparser/Cprint.mli index 349b5f9a..fe71e4fe 100644 --- a/cparser/Cprint.mli +++ b/cparser/Cprint.mli @@ -20,6 +20,7 @@ val print_debug_idents : bool ref val location : Format.formatter -> C.location -> unit val attributes : Format.formatter -> C.attributes -> unit val typ : Format.formatter -> C.typ -> unit +val typ_raw : Format.formatter -> C.typ -> unit val simple_decl : Format.formatter -> C.ident * C.typ -> unit val full_decl: Format.formatter -> C.decl -> unit val const : Format.formatter -> C.constant -> unit diff --git a/cparser/Elab.ml b/cparser/Elab.ml index e3a0ef0c..52426014 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -42,8 +42,8 @@ let warning loc = let print_typ env fmt ty = match ty with | TNamed _ -> - Format.fprintf fmt "'%a' (aka '%a')" Cprint.typ ty Cprint.typ (Cutil.unroll env ty) - | _ -> Format.fprintf fmt "'%a'" Cprint.typ ty + Format.fprintf fmt "'%a' (aka '%a')" Cprint.typ_raw ty Cprint.typ_raw (Cutil.unroll env ty) + | _ -> Format.fprintf fmt "'%a'" Cprint.typ_raw ty (* Error reporting for Env functions *) -- cgit From 0c45b5422ef0905941a00c011d34543d678c8135 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 29 Aug 2016 17:51:43 +0200 Subject: Fixed types in Elab.ml. Bug 18004 --- cparser/Elab.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index f16a057a..3d50c3b6 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -508,7 +508,7 @@ let rec elab_specifier keep_ty ?(only = false) loc env specifier = attr := add_attributes (elab_cvspec env cv) !attr | SpecStorage st -> if !sto <> Storage_default && st <> TYPEDEF then - error loc "multiple storage classes in declaration specifiers"; + error loc "multiple storage classes in declaration specifier"; begin match st with | AUTO -> () | STATIC -> sto := Storage_static @@ -787,7 +787,7 @@ and elab_field_group keep_ty env (Field_group (spec, fieldlist, loc)) = | _ -> ILongLong (* trigger next error message *) in if integer_rank ik > integer_rank IInt then begin error loc - "the type of bitfield '%s' must be an integer type no bigger than 'int'" id; + "the type of bit-field '%s' must be an integer type no bigger than 'int'" id; None end else begin let expr,env' =(!elab_expr_f loc env sz) in @@ -1266,7 +1266,7 @@ and elab_item zi item il = elab_list zi il false | CWStr s, TInt(_, _) when compatible_types AttrIgnoreTop env ty_elt (TInt(wchar_ikind(), [])) -> if not (I.index_below (Int64.of_int(List.length s - 1)) sz) then - warning loc Unnamed "initializer string for array of wide chars is too long"; + warning loc Unnamed "initializer-string for array of wide chars is too long"; elab_list (I.set zi (init_int_array_wstring sz s)) il false | CWStr _, _ -> error loc "initialization of an array of non-wchar_t elements with a wide string literal"; @@ -1470,7 +1470,7 @@ let elab_expr vararg loc env a = let ty = match b3.edesc with ESizeof ty -> ty | _ -> assert false in let ty' = default_argument_conversion env ty in if not (compatible_types AttrIgnoreTop env ty ty') then - warning Varargs "second argument of va_rarg is of promotable type %a; this var_arg has undefined behavior because arguments will be promoted to %a" + warning Varargs "second argument to 'va_arg' is of promotable type %a; this va_arg has undefined behavior because arguments will be promoted to %a" (print_typ env) ty (print_typ env) ty'; { edesc = ECall(ident, [b2; b3]); etyp = ty },env @@ -1857,7 +1857,7 @@ let elab_expr vararg loc env a = if not (is_modifiable_lvalue env b1) then err "expression is not assignable"; if not (is_scalar_type env b1.etyp) then - err "cannot %s value of type %a" msg (print_typ env) b1.etyp; + err "cannot %s value of type %a" msg (print_typ env) b1.etyp; { edesc = EUnop(op, b1); etyp = b1.etyp },env (* Elaboration of binary operators over integers *) -- cgit From 082b69414e8b861286139fe7848561893d3f3702 Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Tue, 30 Aug 2016 10:33:26 +0200 Subject: bug 18004, fix some typos/grammar --- cparser/Elab.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 3d50c3b6..7cbe4c7b 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -794,7 +794,7 @@ and elab_field_group keep_ty env (Field_group (spec, fieldlist, loc)) = match Ceval.integer_expr env' expr with | Some n -> if n < 0L then begin - error loc "bit-filed '%s' has negative width (%Ld)" id n; + error loc "bit-field '%s' has negative width (%Ld)" id n; None end else let max = Int64.of_int(sizeof_ikind ik * 8) in @@ -808,7 +808,7 @@ and elab_field_group keep_ty env (Field_group (spec, fieldlist, loc)) = end else Some(Int64.to_int n) | None -> - error loc "bit-field '%s' witdth not an integer constant" id; + error loc "bit-field '%s' width not an integer constant" id; None end in { fld_name = id; fld_typ = ty; fld_bitfield = optbitsize' } @@ -1199,7 +1199,7 @@ let rec elab_designator loc env zi desig = | Some zi' -> elab_designator loc env zi' desig' | None -> - error loc "field designator '%s' does not have refer to any field in type '%s'" name (I.name zi); + error loc "field designator '%s' does not refer to any field in type '%s'" name (I.name zi); raise Exit end | ATINDEX_INIT a :: desig' -> @@ -1992,7 +1992,7 @@ let enter_typedefs loc env sto dl = if equal_types env ty ty' then env else begin - error loc "typdef redefinition with different types (%a vs %a)" + error loc "typedef redefinition with different types (%a vs %a)" (print_typ env) ty (print_typ env) ty'; env end -- cgit From 4a27ac909430e949c4ee0c155fd90ecd5709fda7 Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Tue, 30 Aug 2016 10:36:30 +0200 Subject: bug 18004, fix some typos/grammar --- cfrontend/C2C.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 4049907e..637c29ec 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -717,7 +717,7 @@ let rec convertExpr env e = let e2' = convertExpr env e2 in if Cutil.is_composite_type env e1.etyp && List.mem AVolatile (Cutil.attributes_of_type env e1.etyp) then - warning Cerrors.Unnamed "assignment to a lvalue of volatile composite type"; + warning Cerrors.Unnamed "assignment to an lvalue of volatile composite type"; ewrap (Ctyping.eassign e1' e2') | C.EBinop((C.Oadd_assign|C.Osub_assign|C.Omul_assign|C.Odiv_assign| C.Omod_assign|C.Oand_assign|C.Oor_assign|C.Oxor_assign| -- cgit From 8c926e846bd36a6e8f0f7820ba98f049d4835095 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 31 Aug 2016 11:03:23 +0200 Subject: Fixed typos. Removed duplicated of, changed string to string literal for wording than the C standard. Bug 18004 --- cfrontend/C2C.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 637c29ec..a7234705 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -357,11 +357,11 @@ let make_builtin_memcpy args = let sz1 = match Initializers.constval !comp_env sz with | Errors.OK(Vint n) -> n - | _ -> error "argument 3 of of '__builtin_memcpy_aligned' must be a constant"; Integers.Int.zero in + | _ -> error "argument 3 of '__builtin_memcpy_aligned' must be a constant"; Integers.Int.zero in let al1 = match Initializers.constval !comp_env al with | Errors.OK(Vint n) -> n - | _ -> error "argument 4 of of '__builtin_memcpy_aligned' must be a constant"; Integers.Int.one in + | _ -> error "argument 4 of '__builtin_memcpy_aligned' must be a constant"; Integers.Int.one in (* to check: sz1 > 0, al1 divides sz1, al1 = 1|2|4|8 *) (* Issue #28: must decay array types to pointer types *) Ebuiltin(EF_memcpy(sz1, al1), @@ -758,12 +758,12 @@ let rec convertExpr env e = let (kind, args1) = match args with | {edesc = C.EConst(CInt(n,_,_))} :: args1 -> (n, args1) - | _ -> error "argument 1 of '__builtin_debug' must be constant"; (1L, args) in + | _ -> error "argument 1 of '__builtin_debug' must be a constant"; (1L, args) in let (text, args2) = match args1 with | {edesc = C.EConst(CStr(txt))} :: args2 -> (txt, args2) | {edesc = C.EVar id} :: args2 -> (id.name, args2) - | _ -> error "argument 2 of '__builtin_debug' must be either a string or variable"; ("", args1) in + | _ -> error "argument 2 of '__builtin_debug' must be either a string literal or a variable"; ("", args1) in let targs2 = convertTypArgs env [] args2 in Ebuiltin( EF_debug(P.of_int64 kind, intern_string text, @@ -778,7 +778,7 @@ let rec convertExpr env e = EF_annot(coqstring_of_camlstring txt, typlist_of_typelist targs1), targs1, convertExprList env args1, convertTyp env e.etyp) | _ -> - error "argument 1 of '__builtin_annot' must be a string"; + error "argument 1 of '__builtin_annot' must be a string literal"; ezero end @@ -944,7 +944,7 @@ let rec contains_case s = | 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' statement not in switch statement" + unsupported "'case' statement not in 'switch' statement" | C.Slabeled(_,s) -> contains_case s | C.Sblock b -> List.iter contains_case b @@ -1004,9 +1004,9 @@ let rec convertStmt env s = | C.Slabeled(C.Slabel lbl, s1) -> Slabel(intern_string lbl, convertStmt env s1) | C.Slabeled(C.Scase _, _) -> - unsupported "'case' statement not in switch statement"; Sskip + unsupported "'case' statement not in 'switch' statement"; Sskip | C.Slabeled(C.Sdefault, _) -> - unsupported "'default' statement not in switch statement"; Sskip + unsupported "'default' statement not in 'switch' statement"; Sskip | C.Sgoto lbl -> Sgoto(intern_string lbl) | C.Sreturn None -> -- cgit From b3e25b456f8e853b2380ede8edd6a9b7e688b780 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 31 Aug 2016 11:06:34 +0200 Subject: Added missing literal. Bug 18004 --- cfrontend/C2C.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index a7234705..952d59e7 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -791,7 +791,7 @@ let rec convertExpr env e = Tcons(targ, Tnil), convertExprList env [arg], convertTyp env e.etyp) | _ -> - error "argument 1 of '__builtin_annot_intval' must be a string"; + error "argument 1 of '__builtin_annot_intval' must be a string literal"; ezero end -- cgit From 13f5abe2a0d38e726249b66be574c82a96fec6e4 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 31 Aug 2016 11:12:13 +0200 Subject: Readded warning about ignored volatile. Bug 18004 --- cfrontend/C2C.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 952d59e7..d7b26322 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -717,7 +717,7 @@ let rec convertExpr env e = let e2' = convertExpr env e2 in if Cutil.is_composite_type env e1.etyp && List.mem AVolatile (Cutil.attributes_of_type env e1.etyp) then - warning Cerrors.Unnamed "assignment to an lvalue of volatile composite type"; + warning Cerrors.Unnamed "assignment to an lvalue of volatile composite type, the 'volatile' qualifier is ignored"; ewrap (Ctyping.eassign e1' e2') | C.EBinop((C.Oadd_assign|C.Osub_assign|C.Omul_assign|C.Odiv_assign| C.Omod_assign|C.Oand_assign|C.Oor_assign|C.Oxor_assign| -- cgit From a0924753089854930e77b0d4c26944a66250d42c Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 31 Aug 2016 11:13:20 +0200 Subject: Updated comment string. Bug 18004. --- cparser/Cutil.ml | 2 +- cparser/Cutil.mli | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index 53142598..f7405098 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -946,7 +946,7 @@ let valid_cast env tfrom tto = | TUnion(s1, _), TUnion(s2, _) -> s1 = s2 | _, _ -> false -(* Check that a cast from the first type to the second is an integer conversion *) +(* Check that the cast from tfrom to tto is an integer to pointer conversion *) let int_pointer_conversion env tfrom tto = match unroll env tfrom, unroll env tto with diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index 7fc6aedd..3f988f7c 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -198,8 +198,8 @@ val valid_assignment : Env.t -> exp -> typ -> bool the given type is allowed. *) val valid_cast : Env.t -> typ -> typ -> bool (* Check that a cast from the first type to the second is allowed. *) -val int_pointer_conversion: Env.t -> typ -> typ -> bool - (* Check that a cast from the first type to the second is an integer +val int_pointer_conversion : Env.t -> typ -> typ -> bool + (* Check that the cast from tfrom to tto is an integer to pointer conversion *) val fundef_typ: fundef -> typ (* Return the function type for the given function definition. *) -- cgit From da89ecda07222548df2dd47332be56dc9de49162 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 31 Aug 2016 12:25:30 +0200 Subject: Restored original bit-field warning. Bug 18004 --- cparser/Bitfields.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml index 4ff4b94c..9f38abc6 100644 --- a/cparser/Bitfields.ml +++ b/cparser/Bitfields.ml @@ -67,7 +67,7 @@ let is_signed_enum_bitfield env sid fld eid n = else if List.for_all (fun (_, v, _) -> int_representable v n true) info.Env.ei_members then true else begin - Cerrors.warning Cutil.no_loc Cerrors.Unnamed "warning: '%s' is narrower than values of its type" fld; + Cerrors.warning Cutil.no_loc Cerrors.Unnamed "not all values of type 'enum %s' can be represented in bit-field '%s' of struct '%s' (%d bits are not enough)" eid.name fld sid.C.name n; false end -- cgit From 2617756dbb2f3bc0765e4276ee95c8cac55ed943 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 31 Aug 2016 15:02:28 +0200 Subject: Reworded errors/warnings in Elab. Some old errors/warnings messages were better before and are now rephrased. Furthermore some formulations are rephrased to match the used formulations of the ISO C stanard, e.g. storage class is replaced with storage-class. Bug 18004 --- cparser/Elab.ml | 136 +++++++++++++++++++++++++++++++------------------------- 1 file changed, 76 insertions(+), 60 deletions(-) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 7cbe4c7b..cca79041 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -508,7 +508,7 @@ let rec elab_specifier keep_ty ?(only = false) loc env specifier = attr := add_attributes (elab_cvspec env cv) !attr | SpecStorage st -> if !sto <> Storage_default && st <> TYPEDEF then - error loc "multiple storage classes in declaration specifier"; + error loc "multiple storage-classes in declaration specifier"; begin match st with | AUTO -> () | STATIC -> sto := Storage_static @@ -695,7 +695,7 @@ and elab_parameter keep_ty env (PARAM (spec, id, decl, attr, loc)) = let ty = add_attributes_type (elab_attributes env attr) ty in if sto <> Storage_default && sto <> Storage_register then error loc - "invalid storage class specifier in function declarator"; + "invalid storage-class specifier in function declarator"; if inl then error loc "'inline' can only appear on functions"; if noret then @@ -1199,21 +1199,21 @@ let rec elab_designator loc env zi desig = | Some zi' -> elab_designator loc env zi' desig' | None -> - error loc "field designator '%s' does not refer to any field in type '%s'" name (I.name zi); + error loc "%s has no member named %s" (I.name zi) name; raise Exit end | ATINDEX_INIT a :: desig' -> let expr,env = (!elab_expr_f loc env a) in begin match Ceval.integer_expr env expr with | None -> - error loc "expression is not an integer constant expression"; + error loc "array element designator for %s is not an integer constant expression" (I.name zi); raise Exit | Some n -> match I.index env zi n with | Some zi' -> elab_designator loc env zi' desig' | None -> - error loc "array index in initializer exceeds array bounds"; + error loc "array index %Ld within %s exceeds array bounds" n (I.name zi); raise Exit end @@ -1259,14 +1259,14 @@ and elab_item zi item il = begin match elab_string_literal loc w s, unroll env ty_elt with | CStr s, TInt((IChar | ISChar | IUChar), _) -> if not (I.index_below (Int64.of_int(String.length s - 1)) sz) then - warning loc Unnamed "initializer-string for array of chars is too long"; + warning loc Unnamed "initializer string for array of chars %s is too long" (I.name zi); elab_list (I.set zi (init_char_array_string sz s)) il false | CStr _, _ -> error loc "initialization of an array of non-char elements with a string literal"; elab_list zi il false | CWStr s, TInt(_, _) when compatible_types AttrIgnoreTop env ty_elt (TInt(wchar_ikind(), [])) -> if not (I.index_below (Int64.of_int(List.length s - 1)) sz) then - warning loc Unnamed "initializer-string for array of wide chars is too long"; + warning loc Unnamed "initializer string for array of wide chars %s is too long" (I.name zi); elab_list (I.set zi (init_int_array_wstring sz s)) il false | CWStr _, _ -> error loc "initialization of an array of non-wchar_t elements with a wide string literal"; @@ -1370,14 +1370,14 @@ let elab_expr vararg loc env a = let warning t fmt = warning loc t fmt in - let check_ptr_arith env ty = + let check_ptr_arith env ty s = match unroll env ty with | TVoid _ -> - err "illegal arithmetic on a pointer to void" + err "illegal arithmetic on a pointer to void in binary '%c'" s | TFun _ -> - err "illegal arithmetic on a pointer to the function type %a" (print_typ env) ty + err "illegal arithmetic on a pointer to the function type %a in binary '%c'" (print_typ env) ty s | _ -> if incomplete_type env ty then - err "arithmetic on a pointer to an incomplete type %a" (print_typ env) ty + err "arithmetic on a pointer to an incomplete type %a in binary '%c'" (print_typ env) ty s in let rec elab env = function @@ -1405,7 +1405,7 @@ let elab_expr vararg loc env a = match (unroll env b1.etyp, unroll env b2.etyp) with | (TPtr(t, _) | TArray(t, _, _)), (TInt _ | TEnum _) -> t | (TInt _ | TEnum _), (TPtr(t, _) | TArray(t, _, _)) -> t - | t1, t2 -> error "subscripted value is not an array, or pointer" in + | t1, t2 -> error "subscripted value is neither an array nor pointer" in { edesc = EBinop(Oindex, b1, b2, TPtr(tres, [])); etyp = tres },env | MEMBEROF(a1, fieldname) -> @@ -1417,7 +1417,7 @@ let elab_expr vararg loc env a = | TUnion(id, attrs) -> (wrap Env.find_union_member loc env (id, fieldname), attrs) | _ -> - error "member reference base type %a is not a structure or union" (print_typ env) b1.etyp in + error "request for member '%s' in something not a structure or union" fieldname in (* A field of a const/volatile struct or union is itself const/volatile *) { edesc = EUnop(Odot fieldname, b1); etyp = add_attributes_type (List.filter attr_inherited_by_members attrs) @@ -1434,7 +1434,7 @@ let elab_expr vararg loc env a = | TUnion(id, attrs) -> (wrap Env.find_union_member loc env (id, fieldname), attrs) | _ -> - error "member reference base type %a is not a struct or union" (print_typ env) b1.etyp + error "request for member '%s' in something not a structure or union" fieldname end | _ -> error "member reference type %a is not a pointer" (print_typ env) b1.etyp in @@ -1497,9 +1497,9 @@ let elab_expr vararg loc env a = | TPtr(ty, a) -> begin match unroll env ty with | TFun(res, args, vararg, a) -> (res, args, vararg) - | _ -> error "called object type %a is not a function or function pointer" (print_typ env) b1.etyp + | _ -> error "called object type %a is neither a function nor function pointer" (print_typ env) b1.etyp end - | _ -> error "called object type %a is not a function or function pointer" (print_typ env) b1.etyp + | _ -> error "called object type %a is neither a function nor function pointer" (print_typ env) b1.etyp in (* Type-check the arguments against the prototype *) let bl',env = @@ -1585,25 +1585,25 @@ let elab_expr vararg loc env a = | UNARY(PLUS, a1) -> let b1,env = elab env a1 in if not (is_arith_type env b1.etyp) then - error "invalid argument type %a to unary expression" (print_typ env) b1.etyp; + error "invalid argument type %a to unary '+'" (print_typ env) b1.etyp; { edesc = EUnop(Oplus, b1); etyp = unary_conversion env b1.etyp },env | UNARY(MINUS, a1) -> let b1,env = elab env a1 in if not (is_arith_type env b1.etyp) then - error "invalid argument type %a to unary expression" (print_typ env) b1.etyp; + error "invalid argument type %a to unary '-'" (print_typ env) b1.etyp; { edesc = EUnop(Ominus, b1); etyp = unary_conversion env b1.etyp },env | UNARY(BNOT, a1) -> let b1,env = elab env a1 in if not (is_integer_type env b1.etyp) then - error "invalid argument type %a to unary expression" (print_typ env) b1.etyp; + error "invalid argument type %a to unary '~'" (print_typ env) b1.etyp; { edesc = EUnop(Onot, b1); etyp = unary_conversion env b1.etyp },env | UNARY(NOT, a1) -> let b1,env = elab env a1 in if not (is_scalar_type env b1.etyp) then - error "invalid argument type %a to unary expression" (print_typ env) b1.etyp; + error "invalid argument type %a to unary '!'" (print_typ env) b1.etyp; { edesc = EUnop(Olognot, b1); etyp = TInt(IInt, []) },env | UNARY(ADDROF, a1) -> @@ -1637,7 +1637,7 @@ let elab_expr vararg loc env a = | TPtr(ty, _) | TArray(ty, _, _) -> { edesc = EUnop(Oderef, b1); etyp = ty },env | _ -> - error "indirection requires pointer operand (%a invalid)" + error "arguemnt of unary '*' is not a pointer (%a invalid)" (print_typ env) b1.etyp end @@ -1649,13 +1649,13 @@ let elab_expr vararg loc env a = (* 6.5.5 to 6.5.12 Binary operator expressions *) | BINARY(MUL, a1, a2) -> - elab_binary_arithmetic Omul a1 a2 + elab_binary_arithmetic "*" Omul a1 a2 | BINARY(DIV, a1, a2) -> - elab_binary_arithmetic Odiv a1 a2 + elab_binary_arithmetic "/" Odiv a1 a2 | BINARY(MOD, a1, a2) -> - elab_binary_integer Omod a1 a2 + elab_binary_integer "%" Omod a1 a2 | BINARY(ADD, a1, a2) -> let b1,env = elab env a1 in @@ -1668,10 +1668,10 @@ let elab_expr vararg loc env a = match unroll env b1.etyp, unroll env b2.etyp with | (TPtr(ty, a) | TArray(ty, _, a)), (TInt _ | TEnum _) -> ty | (TInt _ | TEnum _), (TPtr(ty, a) | TArray(ty, _, a)) -> ty - | _, _ -> error "invalid operands to binary expression (%a and %a)" + | _, _ -> error "invalid operands to binary '+' (%a and %a)" (print_typ env) b1.etyp (print_typ env) b2.etyp in - check_ptr_arith env ty; + check_ptr_arith env ty '+'; TPtr(ty, []) end in { edesc = EBinop(Oadd, b1, b2, tyres); etyp = tyres },env @@ -1690,27 +1690,27 @@ let elab_expr vararg loc env a = err "illegal pointer arithmetic in binary '-'"; (TPtr(ty, []), TPtr(ty, [])) | (TInt _ | TEnum _), (TPtr(ty, a) | TArray(ty, _, a)) -> - check_ptr_arith env ty; + check_ptr_arith env ty '-'; (TPtr(ty, []), TPtr(ty, [])) | (TPtr(ty1, a1) | TArray(ty1, _, a1)), (TPtr(ty2, a2) | TArray(ty2, _, a2)) -> if not (compatible_types AttrIgnoreAll env ty1 ty2) then err "%a and %a are not pointers to compatible types" (print_typ env) b1.etyp (print_typ env) b1.etyp; - check_ptr_arith env ty1; + check_ptr_arith env ty1 '-'; if wrap sizeof loc env ty1 = Some 0 then err "subtraction between two pointers to zero-sized objects"; (TPtr(ty1, []), TInt(ptrdiff_t_ikind(), [])) - | _, _ -> error "invalid operands to binary expression (%a and %a)" + | _, _ -> error "invalid operands to binary '-' (%a and %a)" (print_typ env) b1.etyp (print_typ env) b2.etyp end in { edesc = EBinop(Osub, b1, b2, tyop); etyp = tyres },env | BINARY(SHL, a1, a2) -> - elab_binary_integer Oshl a1 a2 + elab_shift "<<" Oshl a1 a2 | BINARY(SHR, a1, a2) -> - elab_binary_integer Oshr a1 a2 + elab_shift ">>" Oshr a1 a2 | BINARY(EQ, a1, a2) -> elab_comparison Oeq a1 a2 @@ -1726,11 +1726,11 @@ let elab_expr vararg loc env a = elab_comparison Oge a1 a2 | BINARY(BAND, a1, a2) -> - elab_binary_integer Oand a1 a2 + elab_binary_integer "&" Oand a1 a2 | BINARY(BOR, a1, a2) -> - elab_binary_integer Oor a1 a2 + elab_binary_integer "|" Oor a1 a2 | BINARY(XOR, a1, a2) -> - elab_binary_integer Oxor a1 a2 + elab_binary_integer "^" Oxor a1 a2 (* 6.5.13 and 6.5.14 Logical operator expressions *) @@ -1745,7 +1745,7 @@ let elab_expr vararg loc env a = let b2,env = elab env a2 in let b3,env = elab env a3 in if not (is_scalar_type env b1.etyp) then - err "used type %a where arithmetic or pointer type is required" + err "first argument of '?:' is not a scalar type (invalid %a)" (print_typ env) b1.etyp; begin match pointer_decay env b2.etyp, pointer_decay env b3.etyp with | (TInt _ | TFloat _ | TEnum _), (TInt _ | TFloat _ | TEnum _) -> @@ -1759,7 +1759,7 @@ let elab_expr vararg loc env a = match combine_types AttrIgnoreAll env (TPtr(ty1, a1)) (TPtr(ty2, a2)) with | None -> - warning Pointer_type_mismatch "pointer type mismatch (%a and %a)" + warning Pointer_type_mismatch "the second and third argument of '?:' have incompatible pointer types (%a and %a)" (print_typ env) pty1 (print_typ env) pty2; (* tolerance *) TPtr(TVoid (add_attributes a1 a2), []) @@ -1773,7 +1773,7 @@ let elab_expr vararg loc env a = | ty1, ty2 -> match combine_types AttrIgnoreAll env ty1 ty2 with | None -> - error "incompatible operand types (%a and %a)" + error "the second and third argument of '?:' incompatible types (%a and %a)" (print_typ env) ty1 (print_typ env) ty2 | Some tyres -> { edesc = EConditional(b1, b2, b3); etyp = tyres },env @@ -1785,7 +1785,7 @@ let elab_expr vararg loc env a = let b1,env = elab env a1 in let b2,env = elab env a2 in if List.mem AConst (attributes_of_type env b1.etyp) then - error "read-only variable is not assignable"; + error "left-hand side of assignment has 'const' type"; if not (is_modifiable_lvalue env b1) then err "expression is not assignable"; if not (wrap2 valid_assignment loc env b2 b1.etyp) then begin @@ -1823,7 +1823,7 @@ let elab_expr vararg loc env a = begin match elab env (BINARY(sop, a1, a2)) with | ({ edesc = EBinop(_, b1, b2, _); etyp = ty } as b),env -> if List.mem AConst (attributes_of_type env b1.etyp) then - err "read-only variable is not assignable"; + err "left-hand side of assignment has 'const' type"; if not (is_modifiable_lvalue env b1) then err "expression is not assignable"; if not (wrap2 valid_assignment loc env b b1.etyp) then begin @@ -1861,25 +1861,35 @@ let elab_expr vararg loc env a = { edesc = EUnop(op, b1); etyp = b1.etyp },env (* Elaboration of binary operators over integers *) - and elab_binary_integer op a1 a2 = + and elab_binary_integer msg op a1 a2 = let b1,env = elab env a1 in let b2,env = elab env a2 in if not ((is_integer_type env b1.etyp) && (is_integer_type env b2.etyp)) then - error "invalid operands to binary expression (%a and %a)" + error "invalid operands to binary '%s' (%a and %a)" msg (print_typ env) b1.etyp (print_typ env) b2.etyp; let tyres = binary_conversion env b1.etyp b2.etyp in { edesc = EBinop(op, b1, b2, tyres); etyp = tyres },env (* Elaboration of binary operators over arithmetic types *) - and elab_binary_arithmetic op a1 a2 = + and elab_binary_arithmetic msg op a1 a2 = let b1,env = elab env a1 in let b2,env = elab env a2 in if not ((is_arith_type env b1.etyp) && (is_arith_type env b2.etyp)) then - error "invalid operands to binary expression (%a and %a)" + error "invalid operands to binary '%s' (%a and %a)" msg (print_typ env) b1.etyp (print_typ env) b2.etyp; let tyres = binary_conversion env b1.etyp b2.etyp in { edesc = EBinop(op, b1, b2, tyres); etyp = tyres },env +(* Elaboration of shift operators *) + and elab_shift msg op a1 a2 = + let b1,env = elab env a1 in + let b2,env = elab env a2 in + if not ((is_integer_type env b1.etyp) && (is_integer_type env b2.etyp)) then + error "invalid operands to '%s' (%a and %a)" msg + (print_typ env) b1.etyp (print_typ env) b2.etyp; + let tyres = unary_conversion env b1.etyp in + { edesc = EBinop(op, b1, b2, tyres); etyp = tyres },env + (* Elaboration of comparisons *) and elab_comparison op a1 a2 = let b1,env = elab env a1 in @@ -1905,7 +1915,7 @@ let elab_expr vararg loc env a = EBinop(op, b1, b2, TPtr(ty1, [])) | TPtr _, (TInt _ | TEnum _) | (TInt _ | TEnum _), TPtr _ -> - warning Unnamed "ordered comparison between pointer and integer (%a and %a)" + warning Unnamed "comparison between pointer and integer (%a and %a)" (print_typ env) b1.etyp (print_typ env) b2.etyp; EBinop(op, b1, b2, TPtr(TVoid [], [])) | ty1, ty2 -> @@ -1983,15 +1993,16 @@ let __func__type_and_init s = let enter_typedefs loc env sto dl = if sto <> Storage_default then - error loc "cannot combine with previous 'typedef' declaration specifier"; + error loc "non-default storage-class on 'typedef' definition"; List.fold_left (fun env (s, ty, init) -> if init <> NO_INIT then error loc "initializer in typedef"; match previous_def Env.lookup_typedef env s with | Some (s',ty') -> - if equal_types env ty ty' then + if equal_types env ty ty' then begin + warning loc Cerrors.Celeven_extension "redefinition of typedef '%s' is C11 extension" s; env - else begin + end else begin error loc "typedef redefinition with different types (%a vs %a)" (print_typ env) ty (print_typ env) ty'; env @@ -2006,7 +2017,7 @@ let enter_typedefs loc env sto dl = let enter_decdefs local loc env sto dl = (* Sanity checks on storage class *) if sto = Storage_register && not local then - fatal_error loc "illegal storage class on file-scoped variable"; + fatal_error loc "'register' storage-class on file-scoped variable"; if sto <> Storage_default && dl = [] then warning loc Missing_declarations "declaration does not declare anything"; let enter_decdef (decls, env) (s, ty, init) = @@ -2015,8 +2026,8 @@ let enter_decdefs local loc env sto dl = error loc "'extern' declaration variable has an initializer"; if local && isfun then begin match sto with - | Storage_static -> error loc "function declared in block scope cannot have 'static' storage class"; - | Storage_register -> error loc "illegal storage class on function"; + | Storage_static -> error loc "function declared in block scope cannot have 'static' storage-class"; + | Storage_register -> error loc "invalid 'register' storage-class on function"; | _ -> () end; (* Local function declarations are always treated as extern *) @@ -2075,7 +2086,7 @@ let elab_KR_function_parameters env params defs loc = if not (List.mem s params) then error loc' "Declaration of '%s' which is not a function parameter" s; if ie <> NO_INIT then - error loc' "parameter '%s' is initialized" s; + error loc' "illegal initialization of parameter '%s'" s; name in (* Extract names and types from the declarations *) @@ -2083,8 +2094,13 @@ let elab_KR_function_parameters env params defs loc = | DECDEF((spec', name_init_list), loc') -> let name_list = List.map extract_name name_init_list in let (paramsenv, sto) = elab_name_group true loc' env (spec', name_list) in - if sto <> Storage_default && sto <> Storage_register then - error loc' "invalid storage class specifier in function declarator"; + begin match sto with + | Storage_extern -> + error loc' "invalid 'extern' storage-class specifier for function parameter" + | Storage_static -> + error loc' "invalid 'static' storage-class specifier for function parameter" + | _ -> () + end; paramsenv | d -> (* Should never be produced by the parser *) fatal_error (get_definitionloc d) @@ -2152,7 +2168,7 @@ let elab_fundef env spec name defs body loc = let (s, sto, inline, noret, ty, kr_params, env1) = elab_fundef_name true env spec name in if sto = Storage_register then - fatal_error loc "illegal storage class on function"; + fatal_error loc "invalid 'register' storage-class on function"; begin match kr_params, defs with | None, d::_ -> error (get_definitionloc d) @@ -2343,7 +2359,7 @@ let rec elab_stmt env ctx s = let a',env = elab_expr ctx.ctx_vararg loc env a in begin match Ceval.integer_expr env a' with | None -> - error loc "expression is not an integer constant expression" + error loc "expression of 'case' label is not an integer constant expression" | Some n -> () end; let s1,env = elab_stmt env ctx s1 in @@ -2363,7 +2379,7 @@ let rec elab_stmt env ctx s = | If(a, s1, s2, loc) -> let a',env = elab_expr ctx.ctx_vararg loc env a in if not (is_scalar_type env a'.etyp) then - error loc "statement requires expression of scalar type (%a invalid)" + error loc "controlling expression of 'if' does not have scalar type (%a invalid)" (print_typ env) a'.etyp; let s1',env = elab_stmt env ctx s1 in let s2',env = @@ -2378,7 +2394,7 @@ let rec elab_stmt env ctx s = | WHILE(a, s1, loc) -> let a',env = elab_expr ctx.ctx_vararg loc env a in if not (is_scalar_type env a'.etyp) then - error loc "statement requires expression of scalar type (%a invalid)" + error loc "controlling expression of 'while' does not have scalar type (%a invalid)" (print_typ env) a'.etyp; let s1',env = elab_stmt env (ctx_loop ctx) s1 in { sdesc = Swhile(a', s1'); sloc = elab_loc loc },env @@ -2387,7 +2403,7 @@ let rec elab_stmt env ctx s = let s1',env = elab_stmt env (ctx_loop ctx) s1 in let a',env = elab_expr ctx.ctx_vararg loc env a in if not (is_scalar_type env a'.etyp) then - error loc "statement requires expression of scalar type (%a invalid)" + error loc "controlling expression of 'while' does not have scalar type (%a invalid)" (print_typ env) a'.etyp; { sdesc = Sdowhile(s1', a'); sloc = elab_loc loc },env @@ -2411,7 +2427,7 @@ let rec elab_stmt env ctx s = | Some a2 -> elab_expr ctx.ctx_vararg loc env' a2 in if not (is_scalar_type env' a2'.etyp) then - error loc "statement requires expression of scalar type (%a invalid)" (print_typ env) a2'.etyp; + error loc "controlling expression of 'for' does not have scalar type (%a invalid)" (print_typ env) a2'.etyp; let a3',env' = elab_for_expr ctx.ctx_vararg loc env' a3 in let s1',env' = elab_stmt env' (ctx_loop ctx) s1 in let sfor = { sdesc = Sfor(a1', a2', a3', s1'); sloc = elab_loc loc } in @@ -2424,7 +2440,7 @@ let rec elab_stmt env ctx s = | SWITCH(a, s1, loc) -> let a',env = elab_expr ctx.ctx_vararg loc env a in if not (is_integer_type env a'.etyp) then - error loc "statement requires expression of integer type (%a invalid)" + error loc "controlling expression of 'switch' does not have integer type (%a invalid)" (print_typ env) a'.etyp; let s1',env = elab_stmt env (ctx_switch ctx) s1 in { sdesc = Sswitch(a', s1'); sloc = elab_loc loc },env -- cgit From c7ea6ababa7e57a3b9c529cfc0617072eaed0701 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 31 Aug 2016 15:46:51 +0200 Subject: Added back logical operator in error. Bug 18004 --- cparser/Elab.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index cca79041..29bce36e 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -1928,7 +1928,7 @@ let elab_expr vararg loc env a = let b1,env = elab env a1 in let b2,env = elab env a2 in if not ((is_scalar_type env b1.etyp) && (is_scalar_type env b2.etyp)) then - error "invalid operands to binary expression (%a and %a)" + error "invalid operands to binary %s (%a and %a)" msg (print_typ env) b1.etyp (print_typ env) b2.etyp; { edesc = EBinop(op, b1, b2, TInt(IInt, [])); etyp = TInt(IInt, []) },env -- cgit From 8763a45b8a5c6d51d53795573179ba66e479f288 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 31 Aug 2016 16:36:39 +0200 Subject: Added conformance warning. This warning should be triggered if a feature is used that is not part of the code CompCert C language. Bug 18004 --- cparser/Cerrors.ml | 2 ++ cparser/Cerrors.mli | 1 + cparser/Elab.ml | 1 + 3 files changed, 4 insertions(+) diff --git a/cparser/Cerrors.ml b/cparser/Cerrors.ml index 046ca9b0..e1848ffa 100644 --- a/cparser/Cerrors.ml +++ b/cparser/Cerrors.ml @@ -67,6 +67,7 @@ type warning_type = | Return_type | Literal_range | Unknown_pragmas + | CompCert_conformance let active_warnings: warning_type list ref = ref [ Unknown_attribute; @@ -106,6 +107,7 @@ let string_of_warning = function | Return_type -> "return-type" | Literal_range -> "literal-range" | Unknown_pragmas -> "unknown-pragmas" + | CompCert_conformance -> "compcert-conformance" let activate_warning w () = if not (List.mem w !active_warnings) then diff --git a/cparser/Cerrors.mli b/cparser/Cerrors.mli index b547188a..1ef8bb21 100644 --- a/cparser/Cerrors.mli +++ b/cparser/Cerrors.mli @@ -43,6 +43,7 @@ type warning_type = | Return_type (** void return in non-void function *) | Literal_range (** literal ranges *) | Unknown_pragmas (** unknown/unsupported pragma *) + | CompCert_conformance (** features that are not part of the CompCert C core language *) val warning : (string * int) -> warning_type -> ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a (** [warning (f,c) w fmt arg1 ... argN] formats the arguments [arg1] to [argN] as warining according to diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 29bce36e..621417ed 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -2186,6 +2186,7 @@ let elab_fundef env spec name defs body loc = | ty, None -> (ty, [],env1) | TFun(ty_ret, None, false, attr), Some params -> + warning loc Cerrors.CompCert_conformance "non-prototype, pre-standard function definition, converting to prototype form"; let (params', extra_decls,env) = elab_KR_function_parameters env params defs loc in (TFun(ty_ret, Some params', inherit_vararg env s sto ty, attr), extra_decls,env) -- cgit From 204469913eaeffa2642268f35d018bc5329f9372 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 31 Aug 2016 16:40:17 +0200 Subject: Fixed error message for & operator. Bug 18004 --- cparser/Elab.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 621417ed..0766d769 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -1609,7 +1609,7 @@ let elab_expr vararg loc env a = | UNARY(ADDROF, a1) -> let b1,env = elab env a1 in if not (is_lvalue b1 || is_function_type env b1.etyp) then - err "cannot take the address of an rvalue of type %a" (print_typ env) b1.etyp; + err "argument of '&' is not an lvalue (invalid %a)" (print_typ env) b1.etyp; begin match b1.edesc with | EVar id -> begin match wrap Env.find_ident loc env id with -- cgit From 4d6c9149ce2ce2dfedd7db4ab9ad2b9e5750607e Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 1 Sep 2016 11:02:21 +0200 Subject: Simplified int to pointer tests. Now the same warning is triggered for both cases, int to ptr and ptr to int. Bug 18004 --- cparser/Cutil.ml | 3 ++- cparser/Elab.ml | 30 +++++++++++++++--------------- 2 files changed, 17 insertions(+), 16 deletions(-) diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index f7405098..19a32a7e 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -950,7 +950,8 @@ let valid_cast env tfrom tto = let int_pointer_conversion env tfrom tto = match unroll env tfrom, unroll env tto with - | (TInt _ | TEnum _),(TPtr _) -> true + | (TInt _ | TEnum _),(TPtr _) + | (TPtr _),(TInt _ | TEnum _) -> true | _,_ -> false (* Construct an integer constant *) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 0766d769..bd5b1700 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -1004,11 +1004,11 @@ let check_init_type loc env a ty = else if wrap2 valid_cast loc env a.etyp ty then if wrap2 int_pointer_conversion loc env a.etyp ty then warning loc Int_conversion - "incompatible integer to pointer conversion initializing %a with an expression of type %a" + "incompatible integer-pointer conversion initializing %a with an expression of type %a" (print_typ env) ty (print_typ env) a.etyp else - warning loc Int_conversion - "incompatible pointer to integer conversion initializing %a with an expression of type %a" + warning loc Unnamed + "incompatible conversion initializing %a with an expression of type %a" (print_typ env) ty (print_typ env) a.etyp else error loc @@ -1792,11 +1792,11 @@ let elab_expr vararg loc env a = if wrap2 valid_cast loc env b2.etyp b1.etyp then if wrap2 int_pointer_conversion loc env b2.etyp b1.etyp then warning Int_conversion - "incompatible integer to pointer conversion assigning to %a from %a" + "incompatible integer-pointer conversion assigning to %a from %a" (print_typ env) b1.etyp (print_typ env) b2.etyp else - warning Int_conversion - "incompatible pointer to integer conversion assgining to %a from %a" + warning Unnamed + "incompatible conversion assgining to %a from %a" (print_typ env) b1.etyp (print_typ env) b2.etyp else err "assigning to %a from incompatible type %a" @@ -1830,11 +1830,11 @@ let elab_expr vararg loc env a = if wrap2 valid_cast loc env ty b1.etyp then if wrap2 int_pointer_conversion loc env ty b1.etyp then warning Int_conversion - "incompatible integer to pointer conversion assigning to %a from %a" + "incompatible integer-pointer conversion assigning to %a from %a" (print_typ env) b1.etyp (print_typ env) ty else - warning Int_conversion - "incompatible pointer to integer conversion assgining to %a from %a" + warning Unnamed + "incompatible conversion assgining to %a from %a" (print_typ env) b1.etyp (print_typ env) ty else err "assigning to %a from incompatible type %a" @@ -1954,11 +1954,11 @@ let elab_expr vararg loc env a = if wrap2 valid_cast loc env ty_a ty_p then begin if wrap2 int_pointer_conversion loc env ty_a ty_p then warning Int_conversion - "incompatible integer to pointer conversion passing %a to parameter of type %a" + "incompatible integer-pointer conversion passing %a to parameter of type %a" (print_typ env) ty_a (print_typ env) ty_p else - warning Int_conversion - "incompatible pointer to integer conversion passing %a to parameter of type %a" + warning Unnamed + "incompatible conversion passing %a to parameter of type %a" (print_typ env) ty_a (print_typ env) ty_p end else err @@ -2473,11 +2473,11 @@ let rec elab_stmt env ctx s = if wrap2 valid_cast loc env b.etyp ctx.ctx_return_typ then if wrap2 int_pointer_conversion loc env b.etyp ctx.ctx_return_typ then warning loc Int_conversion - "incompatible integer to pointer conversion returning %a from a function with result type %a" + "incompatible integer-pointer conversion returning %a from a function with result type %a" (print_typ env) b.etyp (print_typ env) ctx.ctx_return_typ else - warning loc Int_conversion - "incompatible integer to pointer conversion returning %a from a function with result type %a" + warning loc Unnamed + "incompatible conversion returning %a from a function with result type %a" (print_typ env) b.etyp (print_typ env) ctx.ctx_return_typ else error loc -- cgit From a4bf0090177fa62a6a6bbce68a7bb6229204494d Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 1 Sep 2016 11:10:16 +0200 Subject: Reworded warning. Bug 18004 --- cparser/Elab.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index bd5b1700..aa11ebf7 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -1004,16 +1004,16 @@ let check_init_type loc env a ty = else if wrap2 valid_cast loc env a.etyp ty then if wrap2 int_pointer_conversion loc env a.etyp ty then warning loc Int_conversion - "incompatible integer-pointer conversion initializing %a with an expression of type %a" - (print_typ env) ty (print_typ env) a.etyp + "incompatible integer-pointer conversion initializer has type %a instead of the expected type %a" + (print_typ env) a.etyp (print_typ env) ty else warning loc Unnamed - "incompatible conversion initializing %a with an expression of type %a" - (print_typ env) ty (print_typ env) a.etyp + "incompatible conversion initializer has type %a instead of the expected type %a" + (print_typ env) a.etyp (print_typ env) ty else error loc - "initializing %a with an expression of incompatible type %a" - (print_typ env) ty (print_typ env) a.etyp + "initializer has type %a instead of the expected type %a" + (print_typ env) a.etyp (print_typ env) ty (* Representing initialization state using zippers *) -- cgit From dbc855fa4558d8a1b4abff4aadee0b79b814f186 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 1 Sep 2016 11:13:07 +0200 Subject: Readded parameter number. Bug 18004 --- cparser/Elab.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index aa11ebf7..4e8adc77 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -1954,16 +1954,16 @@ let elab_expr vararg loc env a = if wrap2 valid_cast loc env ty_a ty_p then begin if wrap2 int_pointer_conversion loc env ty_a ty_p then warning Int_conversion - "incompatible integer-pointer conversion passing %a to parameter of type %a" - (print_typ env) ty_a (print_typ env) ty_p + "incompatible integer-pointer conversion passing %a to parameter %d of type %a" + (print_typ env) ty_a argno (print_typ env) ty_p else warning Unnamed - "incompatible conversion passing %a to parameter of type %a" - (print_typ env) ty_a (print_typ env) ty_p end + "incompatible conversion passing %a to parameter %d of type %a" + (print_typ env) ty_a argno (print_typ env) ty_p end else err - "passing %a to parameter of incompatible type %a" - (print_typ env) ty_a (print_typ env) ty_p + "passing %a to parameter %d of incompatible type %a" + (print_typ env) ty_a argno (print_typ env) ty_p end; let rest,env = elab_arguments (argno + 1) (argl,env) paraml vararg in arg1 :: rest,env -- cgit From 20f226ce463221032238895264c73d2207bf31d8 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 5 Sep 2016 09:18:36 +0200 Subject: Fixed typos and reverted error message. Bug 18004 --- cparser/Elab.ml | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 4e8adc77..39cb36b1 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -1470,8 +1470,8 @@ let elab_expr vararg loc env a = let ty = match b3.edesc with ESizeof ty -> ty | _ -> assert false in let ty' = default_argument_conversion env ty in if not (compatible_types AttrIgnoreTop env ty ty') then - warning Varargs "second argument to 'va_arg' is of promotable type %a; this va_arg has undefined behavior because arguments will be promoted to %a" - (print_typ env) ty (print_typ env) ty'; + warning Varargs "%a is promoted to %a when passed through '...'. You should pass %a, not %a, to 'va_arg'" + (print_typ env) ty (print_typ env) ty' (print_typ env) ty' (print_typ env) ty; { edesc = ECall(ident, [b2; b3]); etyp = ty },env | CALL(a1, al) -> @@ -1527,7 +1527,7 @@ let elab_expr vararg loc env a = err "operand of type %a where arithmetic or pointer type is required" (print_typ env) b1.etyp | TFloat _, TPtr _ -> - err "operand of type %a cannot be cast to a pointer typ" + err "operand of type %a cannot be cast to a pointer type" (print_typ env) b1.etyp | TPtr _ , TFloat _ -> err "pointer cannot be cast to type %a" (print_typ env) ty @@ -1792,11 +1792,11 @@ let elab_expr vararg loc env a = if wrap2 valid_cast loc env b2.etyp b1.etyp then if wrap2 int_pointer_conversion loc env b2.etyp b1.etyp then warning Int_conversion - "incompatible integer-pointer conversion assigning to %a from %a" + "incompatible integer-pointer conversion: assigning to %a from %a" (print_typ env) b1.etyp (print_typ env) b2.etyp else warning Unnamed - "incompatible conversion assgining to %a from %a" + "incompatible conversion assigning to %a from %a" (print_typ env) b1.etyp (print_typ env) b2.etyp else err "assigning to %a from incompatible type %a" @@ -1830,11 +1830,11 @@ let elab_expr vararg loc env a = if wrap2 valid_cast loc env ty b1.etyp then if wrap2 int_pointer_conversion loc env ty b1.etyp then warning Int_conversion - "incompatible integer-pointer conversion assigning to %a from %a" + "incompatible integer-pointer conversion: assigning to %a from %a" (print_typ env) b1.etyp (print_typ env) ty else warning Unnamed - "incompatible conversion assgining to %a from %a" + "incompatible conversion assigning to %a from %a" (print_typ env) b1.etyp (print_typ env) ty else err "assigning to %a from incompatible type %a" @@ -1954,7 +1954,7 @@ let elab_expr vararg loc env a = if wrap2 valid_cast loc env ty_a ty_p then begin if wrap2 int_pointer_conversion loc env ty_a ty_p then warning Int_conversion - "incompatible integer-pointer conversion passing %a to parameter %d of type %a" + "incompatible integer-pointer conversion: passing %a to parameter %d of type %a" (print_typ env) ty_a argno (print_typ env) ty_p else warning Unnamed @@ -2473,7 +2473,7 @@ let rec elab_stmt env ctx s = if wrap2 valid_cast loc env b.etyp ctx.ctx_return_typ then if wrap2 int_pointer_conversion loc env b.etyp ctx.ctx_return_typ then warning loc Int_conversion - "incompatible integer-pointer conversion returning %a from a function with result type %a" + "incompatible integer-pointer conversion: returning %a from a function with result type %a" (print_typ env) b.etyp (print_typ env) ctx.ctx_return_typ else warning loc Unnamed -- cgit