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"

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