From b55fa30ad44a647aca8ae8786da2d4cc1a881cd8 Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Fri, 14 Sep 2018 13:55:02 +0200 Subject: Improved diagnostics: spelling, wording, etc (#138) * bug 24268: avoid assertion after reporting error for invalid call to builtin_debug * bug 24268, remove duplicated warning tag in lexer messages * bug 24268, fix spelling in array element designator message * bug 24268, unify 'consider adding option ...' messages * bug 24268, add spacing for icbi operands * bug 24268, uniform use of Ignored_attributes class for identical warnings * bug 24268, unify message for 'assignment to const type' to error from error/fatal error * bug 24268, in handcrafted.messages, "a xxx have been recognized" -> "a xxx has been recognized" --- cfrontend/C2C.ml | 16 ++++++++-------- cparser/Elab.ml | 8 ++++---- cparser/Lexer.mll | 2 +- cparser/handcrafted.messages | 2 +- powerpc/TargetPrinter.ml | 2 +- 5 files changed, 15 insertions(+), 15 deletions(-) diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 1bbcb146..d6bf76f3 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -318,7 +318,7 @@ let attributes = [ ("section", Cutil.Attr_name); ("unused", Cutil.Attr_name) ] - + (** ** Functions used to handle string literals *) @@ -546,14 +546,14 @@ let convertFkind k a : coq_type = let checkFunctionType env tres targs = if not !Clflags.option_fstruct_passing then begin if Cutil.is_composite_type env tres then - unsupported "function returning a struct or union (consider adding option -fstruct-passing)"; + unsupported "function returning a struct or union (consider adding option [-fstruct-passing])"; begin match targs with | None -> () | Some l -> List.iter (fun (id, ty) -> if Cutil.is_composite_type env ty then - unsupported "function parameter of struct or union type (consider adding option -fstruct-passing)") + unsupported "function parameter of struct or union type (consider adding option [-fstruct-passing])") l end end @@ -606,12 +606,12 @@ let rec convertTypArgs env tl el = let convertField env f = if f.fld_bitfield <> None then - unsupported "bit field in struct or union (consider adding option -fbitfields)"; + unsupported "bit field in struct or union (consider adding option [-fbitfields])"; (intern_string f.fld_name, convertTyp env f.fld_typ) let convertCompositedef env su id attr members = if Cutil.find_custom_attributes ["packed";"__packed__"] attr <> [] then - unsupported "packed struct (consider adding option -fpacked-structs)"; + unsupported "packed struct (consider adding option [-fpacked-structs])"; let t = match su with | C.Struct -> let layout = Cutil.struct_layout env attr members in @@ -829,10 +829,10 @@ let rec convertExpr env e = | C.ECompound(ty1, ie) -> unsupported "compound literals"; ezero + | C.ECall({edesc = C.EVar {name = "__builtin_debug"}}, args) when List.length args < 2 -> + error "too few arguments to function call, expected at least 2, have 0"; + ezero | C.ECall({edesc = C.EVar {name = "__builtin_debug"}}, args) -> - let len = List.length args in - if len < 2 then - error "too few arguments to function call, expected at least 2, have 0"; let (kind, args1) = match args with | {edesc = C.EConst(CInt(n,_,_))} :: args1 when n <> 0L-> (n, args1) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index b35963f7..718261b4 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -160,7 +160,7 @@ let combine_toplevel_definitions loc env s old_sto old_ty sto ty = let old_attrs = attributes_of_type env old_ty and new_attrs = attributes_of_type env ty in if not (Cutil.incl_attributes new_attrs old_attrs) then - warning loc Ignored_attributes "attribute declaration must precede definition" + warning loc Ignored_attributes "attribute declaration must precede definition" end; let new_sto = (* The only case not allowed is removing static *) @@ -1080,7 +1080,7 @@ and elab_struct_or_union_info kind loc env members attrs = and elab_struct_or_union only kind loc tag optmembers attrs env = let warn_attrs () = if attrs <> [] then - warning loc Unnamed "attribute declaration must precede definition" in + warning loc Ignored_attributes "attribute declaration must precede definition" in let optbinding, tag = match tag with | None -> None, "" @@ -1920,7 +1920,7 @@ let elab_expr ctx loc env a = | ATINDEX_INIT e,TArray (sub_ty,_,_) -> let e,env = elab env e in let e = match Ceval.integer_expr env e with - | None -> fatal_error "array element designator for is not an integer constant expression" + | None -> fatal_error "array element designator is not an integer constant expression" | Some n-> n in let size = match sizeof env sub_ty with | None -> assert false (* We expect only complete types *) @@ -2137,7 +2137,7 @@ let elab_expr ctx 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 - fatal_error "left-hand side of assignment has 'const' type"; + error "left-hand side of assignment has 'const' type"; if not (is_modifiable_lvalue env b1) then error "expression is not assignable"; if not (wrap2 valid_assignment loc env b2 b1.etyp) then begin diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll index 357c6c50..b2a668f0 100644 --- a/cparser/Lexer.mll +++ b/cparser/Lexer.mll @@ -135,7 +135,7 @@ let error lb fmt = let warning lb fmt = Diagnostics.warning - (lb.lex_curr_p.pos_fname,lb.lex_curr_p.pos_lnum) Diagnostics.Unnamed ("warning: " ^^ fmt) + (lb.lex_curr_p.pos_fname,lb.lex_curr_p.pos_lnum) Diagnostics.Unnamed fmt (* Simple character escapes *) diff --git a/cparser/handcrafted.messages b/cparser/handcrafted.messages index 16dbb2a0..95077739 100644 --- a/cparser/handcrafted.messages +++ b/cparser/handcrafted.messages @@ -2664,7 +2664,7 @@ translation_unit_file: INT LPAREN PRE_NAME VAR_NAME SEMICOLON ## In state 261, spurious reduction of production declarator -> declarator_noattrend attribute_specifier_list ## -Up to this point, a declarator have been recognized: +Up to this point, a declarator has been recognized: $0 If this declarator is complete, then at this point, a closing parenthesis ')' is expected. diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index d8b0ee4b..c1aaa55d 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -605,7 +605,7 @@ module Target (System : SYSTEM):TARGET = | Pisel (r1,r2,r3,cr) -> fprintf oc " isel %a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 crbit cr | Picbi (r1,r2) -> - fprintf oc " icbi %a,%a\n" ireg r1 ireg r2 + fprintf oc " icbi %a, %a\n" ireg r1 ireg r2 | Picbtls (n,r1,r2) -> fprintf oc " icbtls %ld, %a, %a\n" (camlint_of_coqint n) ireg r1 ireg r2 | Pisync -> -- cgit