From d13f1e243ff5ac94ecfc64f2bd81ae5d1c33bfcc Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Mon, 4 Jun 2018 14:47:16 +0200 Subject: Various improvements in the wording of diagnostics. Fix various typos in diagnostic messages and unified wording and capitalization. Bug 23850 --- backend/Regalloc.ml | 8 +-- cparser/Elab.ml | 147 +++++++++++++++++++++++++------------------------- cparser/Lexer.mll | 6 +-- cparser/Parse.ml | 2 +- cparser/Unblock.ml | 2 +- debug/DwarfPrinter.ml | 2 +- driver/Assembler.mli | 2 +- driver/Commandline.ml | 12 ++--- driver/Driver.ml | 2 +- driver/Driveraux.ml | 2 +- driver/Frontend.mli | 2 +- driver/Linker.mli | 4 +- lib/Readconfig.mll | 6 +-- 13 files changed, 98 insertions(+), 99 deletions(-) diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml index d4d7362d..19aba4f6 100644 --- a/backend/Regalloc.ml +++ b/backend/Regalloc.ml @@ -644,7 +644,7 @@ let add_interfs_instr g instr live = (* Reloads from incoming slots can occur when some 64-bit parameters are split and passed as two 32-bit stack locations. *) begin match src with - | L(Locations.S(Incoming, _, _)) -> + | L(Locations.S(Incoming, _, _)) -> add_interfs_def g (vmreg temp_for_parent_frame) live | _ -> () end @@ -1210,9 +1210,9 @@ let regalloc f = Errors.OK(first_round f3 liveness) with | Timeout -> - Errors.Error(Errors.msg (coqstring_of_camlstring "Spilling fails to converge")) + Errors.Error(Errors.msg (coqstring_of_camlstring "spilling fails to converge")) | Type_error_at pc -> - Errors.Error [Errors.MSG(coqstring_of_camlstring "Ill-typed XTL code at PC "); + Errors.Error [Errors.MSG(coqstring_of_camlstring "ill-typed XTL code at PC "); Errors.POS pc] | Bad_LTL -> - Errors.Error(Errors.msg (coqstring_of_camlstring "Bad LTL after spilling")) + Errors.Error(Errors.msg (coqstring_of_camlstring "bad LTL after spilling")) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 8a643362..d0de1058 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -832,7 +832,7 @@ and elab_fundef_name env spec (Name (s, decl, attr, loc)) = if tydef then error loc "'typedef' is forbidden here"; let id = Env.fresh_ident s in - let ((ty, kr_params), env'') = + let ((ty, kr_params), env'') = elab_type_declarator ~fundef:true loc env' bty decl in let a = elab_attributes env attr in (id, sto, inl, noret, add_attributes_type a ty, kr_params, env', env'') @@ -1020,7 +1020,7 @@ and elab_struct_or_union only kind loc tag optmembers attrs env = | Some(tag', ({Env.ci_sizeof = None} as ci)), Some members when Env.in_current_scope env tag' -> if ci.Env.ci_kind <> kind then - error loc "use of '%s' with tag type that does not match previous declaration" tag; + fatal_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 *) @@ -1075,7 +1075,7 @@ and elab_enum_item env ((s, exp), loc) nextval = if redef Env.lookup_typedef env s then 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 Constant_conversion "integer literal '%Ld' is too large to be represented in any integer type" + warning loc Constant_conversion "integer literal '%Ld' is too large to be represented in the enumeration integer type" v; let (id, env') = Env.enter_enum_item env s v in ((id, v, exp'), Int64.succ v, env') @@ -1157,11 +1157,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-pointer conversion initializer has type %a instead of the expected type %a" + "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 initializer has type %a instead of the expected type %a" + "incompatible conversion: initializer has type %a instead of the expected type %a" (print_typ env) a.etyp (print_typ env) ty else error loc @@ -1586,19 +1586,18 @@ let ctx_constexp = { let elab_expr ctx loc env a = - let err fmt = error loc fmt in (* non-fatal error *) - let error fmt = fatal_error loc fmt in - let warning t fmt = - warning loc t fmt in + let error fmt = error loc fmt in + let fatal_error fmt = fatal_error loc fmt in + let warning t fmt = warning loc t fmt in let check_ptr_arith env ty s = match unroll env ty with | TVoid _ -> - err "illegal arithmetic on a pointer to void in binary '%c'" s + error "illegal arithmetic on a pointer to void in binary '%c'" s | TFun _ -> - err "illegal arithmetic on a pointer to the function type %a in binary '%c'" (print_typ env) ty s + error "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 in binary '%c'" (print_typ env) ty s + error "arithmetic on a pointer to an incomplete type %a in binary '%c'" (print_typ env) ty s in let check_static_var id sto ty = @@ -1634,7 +1633,7 @@ let elab_expr ctx 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 neither an array nor pointer" in + | t1, t2 -> fatal_error "subscripted value is neither an array nor pointer" in { edesc = EBinop(Oindex, b1, b2, TPtr(tres, [])); etyp = tres },env | MEMBEROF(a1, fieldname) -> @@ -1646,7 +1645,7 @@ let elab_expr ctx loc env a = | TUnion(id, attrs) -> (wrap Env.find_union_member loc env (id, fieldname), attrs) | _ -> - error "request for member '%s' in something not a structure or union" fieldname in + fatal_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 *) let rec access = function | [] -> b1 @@ -1668,10 +1667,10 @@ let elab_expr ctx loc env a = | TUnion(id, attrs) -> (wrap Env.find_union_member loc env (id, fieldname), attrs) | _ -> - error "request for member '%s' in something not a structure or union" fieldname + fatal_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 + fatal_error "member reference type %a is not a pointer" (print_typ env) b1.etyp in let rec access = function | [] -> assert false | [fld] -> @@ -1695,7 +1694,7 @@ let elab_expr ctx loc env a = *) | CALL((VARIABLE "__builtin_va_start" as a1), [a2; a3]) -> if not ctx.ctx_vararg then - err "'va_start' used in function with fixed args"; + error "'va_start' used in function with fixed args"; let b1,env = elab env a1 in let b2,env = elab env a2 in let _b3,env = elab env a3 in @@ -1740,9 +1739,9 @@ let elab_expr ctx 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 neither a function nor function pointer" (print_typ env) b1.etyp + | _ -> fatal_error "called object type %a is neither a function nor function pointer" (print_typ env) b1.etyp end - | _ -> error "called object type %a is neither a function nor function pointer" (print_typ env) b1.etyp + | _ -> fatal_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 = @@ -1764,18 +1763,18 @@ let elab_expr ctx loc env a = if not (wrap2 valid_cast loc env b1.etyp ty) then begin match unroll env b1.etyp, unroll env ty with | _, (TStruct _|TUnion _ | TVoid _) -> - err "used type %a where arithmetic or pointer type is required" + error "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" + error "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 type" + error "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 + error "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 + error "illegal cast from %a to %a" (print_typ env) b1.etyp (print_typ env) ty end; { edesc = ECast(ty, b1); etyp = ty },env @@ -1785,7 +1784,7 @@ let elab_expr ctx loc env a = let (ty, env) = elab_type loc env spec dcl in begin match elab_initializer loc env "" ty ie with | (ty', Some i) -> { edesc = ECompound(ty', i); etyp = ty' },env - | (ty', None) -> error "ill-formed compound literal" + | (ty', None) -> fatal_error "ill-formed compound literal" end (* 6.5.3 Unary expressions *) @@ -1793,33 +1792,33 @@ let elab_expr ctx loc env a = | EXPR_SIZEOF a1 -> let b1,env = elab env a1 in if wrap incomplete_type loc env b1.etyp then - error "invalid application of 'sizeof' to an incomplete type %a" (print_typ env) b1.etyp; + fatal_error "invalid application of 'sizeof' to an incomplete type %a" (print_typ env) b1.etyp; if wrap is_bitfield loc env b1 then - error "invalid application of 'sizeof' to a bit-field"; + fatal_error "invalid application of 'sizeof' to a bit-field"; { edesc = ESizeof b1.etyp; etyp = TInt(size_t_ikind(), []) },env | TYPE_SIZEOF (spec, dcl) -> let (ty, env') = elab_type loc env spec dcl in if wrap incomplete_type loc env' ty then - error "invalid application of 'sizeof' to an incomplete type %a" (print_typ env) ty; + fatal_error "invalid application of 'sizeof' to an incomplete type %a" (print_typ env) ty; { edesc = ESizeof ty; etyp = TInt(size_t_ikind(), []) },env' | ALIGNOF (spec, dcl) -> let (ty, env') = elab_type loc env spec dcl in warning Celeven_extension "'_Alignof' is a C11 extension"; if wrap incomplete_type loc env' ty then - error "invalid application of '_Alignof' to an incomplete type %a" (print_typ env) ty; + fatal_error "invalid application of 'alignof' to an incomplete type %a" (print_typ env) ty; { edesc = EAlignof ty; etyp = TInt(size_t_ikind(), []) },env' | BUILTIN_OFFSETOF ((spec,dcl), mem) -> let (ty,env) = elab_type loc env spec dcl in if incomplete_type env ty then - error "offsetof of incomplete type %a" (print_typ env) ty; + fatal_error "offsetof of incomplete type %a" (print_typ env) ty; let members env ty mem = match ty with | TStruct (id,_) -> wrap Env.find_struct_member loc env (id,mem) | TUnion (id,_) -> wrap Env.find_union_member loc env (id,mem) - | _ -> error "request for member '%s' in something not a structure or union" mem in + | _ -> fatal_error "request for member '%s' in something not a structure or union" mem in let rec offset_of_list acc env ty = function | [] -> acc,ty | fld::rest -> let off = offsetof env ty fld in @@ -1834,16 +1833,16 @@ 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 -> error "array element designator for is not an integer constant expression" + | None -> fatal_error "array element designator for 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 *) | Some s -> s in let off_accu = match cautious_mul e size with - | None -> error "'offsetof' overflows" + | None -> fatal_error "'offsetof' overflows" | Some s -> off_accu + s in env,off_accu,sub_ty - | ATINDEX_INIT _,_ -> error "subscripted value is not an array" in + | ATINDEX_INIT _,_ -> fatal_error "subscripted value is not an array" in let env,offset,_ = List.fold_left offset_of_member (env,0,ty) mem in let size_t = size_t_ikind () in let offset = Ceval.normalize_int (Int64.of_int offset) size_t in @@ -1853,46 +1852,46 @@ let elab_expr ctx 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 '+'" (print_typ env) b1.etyp; + fatal_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 '-'" (print_typ env) b1.etyp; + fatal_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 '~'" (print_typ env) b1.etyp; + fatal_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 '!'" (print_typ env) b1.etyp; + fatal_error "invalid argument type %a to unary '!'" (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 lvalue (invalid %a)" (print_typ env) b1.etyp; + error "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 | Env.II_ident(Storage_register, _) -> - err "address of register variable '%s' requested" id.C.name + error "address of register variable '%s' requested" id.C.name | _ -> () end | EUnop(Odot f, b2) -> let fld = wrap2 field_of_dot_access loc env b2.etyp f in if fld.fld_bitfield <> None then - err "address of bit-field '%s' requested" f + error "address of bit-field '%s' requested" f | EUnop(Oarrow f, b2) -> let fld = wrap2 field_of_arrow_access loc env b2.etyp f in if fld.fld_bitfield <> None then - err "address of bit-field '%s' requested" f + error "address of bit-field '%s' requested" f | _ -> () end; { edesc = EUnop(Oaddrof, b1); etyp = TPtr(b1.etyp, []) },env @@ -1905,7 +1904,7 @@ let elab_expr ctx loc env a = | TPtr(ty, _) | TArray(ty, _, _) -> { edesc = EUnop(Oderef, b1); etyp = ty },env | _ -> - error "arguemnt of unary '*' is not a pointer (%a invalid)" + fatal_error "argument of unary '*' is not a pointer (%a invalid)" (print_typ env) b1.etyp end @@ -1936,7 +1935,7 @@ let elab_expr ctx 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 '+' (%a and %a)" + | _, _ -> fatal_error "invalid operands to binary '+' (%a and %a)" (print_typ env) b1.etyp (print_typ env) b2.etyp in check_ptr_arith env ty '+'; @@ -1955,19 +1954,19 @@ let elab_expr ctx loc env a = match wrap unroll loc env b1.etyp, wrap unroll loc env b2.etyp with | (TPtr(ty, a) | TArray(ty, _, a)), (TInt _ | TEnum _) -> if not (wrap pointer_arithmetic_ok loc env ty) then - err "illegal pointer arithmetic in binary '-'"; + error "illegal pointer arithmetic in binary '-'"; (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" + error "%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 ty2 '-'; if wrap sizeof loc env ty1 = Some 0 then - err "subtraction between two pointers to zero-sized objects"; + error "subtraction between two pointers to zero-sized objects"; (TPtr(ty1, []), TInt(ptrdiff_t_ikind(), [])) - | _, _ -> error "invalid operands to binary '-' (%a and %a)" + | _, _ -> fatal_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 @@ -2011,7 +2010,7 @@ let elab_expr ctx 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 "first argument of '?:' is not a scalar type (invalid %a)" + error "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 _) -> @@ -2039,7 +2038,7 @@ let elab_expr ctx loc env a = | ty1, ty2 -> match combine_types AttrIgnoreAll env ty1 ty2 with | None -> - error "the second and third argument of '?:' incompatible types (%a and %a)" + fatal_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 @@ -2051,9 +2050,9 @@ 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 - error "left-hand side of assignment has 'const' type"; + fatal_error "left-hand side of assignment has 'const' type"; if not (is_modifiable_lvalue env b1) then - err "expression is not assignable"; + error "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 if wrap2 int_pointer_conversion loc env b2.etyp b1.etyp then @@ -2062,10 +2061,10 @@ let elab_expr ctx loc env a = (print_typ env) b1.etyp (print_typ env) b2.etyp else warning Unnamed - "incompatible conversion assigning 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" + error "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 @@ -2089,9 +2088,9 @@ let elab_expr ctx 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"; + error "left-hand side of assignment has 'const' type"; if not (is_modifiable_lvalue env b1) then - err "expression is not assignable"; + error "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 if wrap2 int_pointer_conversion loc env ty b1.etyp then @@ -2100,10 +2099,10 @@ let elab_expr ctx loc env a = (print_typ env) b1.etyp (print_typ env) ty else warning Unnamed - "incompatible conversion assigning 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" + error "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 @@ -2122,9 +2121,9 @@ let elab_expr ctx loc env a = 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 "expression is not assignable"; + error "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; + error "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 *) @@ -2132,7 +2131,7 @@ let elab_expr ctx loc env a = 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 '%s' (%a and %a)" msg + fatal_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 @@ -2142,7 +2141,7 @@ let elab_expr ctx loc env a = 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 '%s' (%a and %a)" msg + fatal_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 @@ -2152,7 +2151,7 @@ let elab_expr ctx loc env a = 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 + fatal_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 @@ -2190,7 +2189,7 @@ let elab_expr ctx loc env 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" + fatal_error "illegal comparison between types@ %a@ and %a" (print_typ env) b1.etyp (print_typ env) b2.etyp; in { edesc = resdesc; etyp = TInt(IInt, []) },env @@ -2199,7 +2198,7 @@ let elab_expr ctx 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 %s (%a and %a)" msg + fatal_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 @@ -2211,14 +2210,14 @@ let elab_expr ctx loc env a = let found = argno - 1 in let expected = List.length params + found in let vararg = if vararg then "at least " else "" in - err "too few arguments to function call, expected %s%d, have %d" vararg expected found; [],env + error "too few arguments to function call, expected %s%d, have %d" vararg expected found; [],env | (_::_,env), [] -> if vararg then 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) + (error "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) @@ -2230,10 +2229,10 @@ let elab_expr ctx loc env a = (print_typ env) ty_a argno (print_typ env) ty_p else warning Unnamed - "incompatible conversion passing %a to parameter %d of type %a" + "incompatible conversion: passing %a to parameter %d of type %a" (print_typ env) ty_a argno (print_typ env) ty_p end else - err + error "passing %a to parameter %d of incompatible type %a" (print_typ env) ty_a argno (print_typ env) ty_p end; @@ -2274,7 +2273,7 @@ let enter_typedefs loc env sto dl = match previous_def Env.lookup_typedef env s with | Some (s',ty') when Env.in_current_scope env s' -> if equal_types env ty ty' then begin - warning loc Celeven_extension "redefinition of typedef '%s' is C11 extension" s; + warning loc Celeven_extension "redefinition of typedef '%s' is a C11 extension" s; env end else begin error loc "typedef redefinition with different types (%a vs %a)" @@ -2312,7 +2311,7 @@ let enter_decdefs local nonstatic_inline loc env sto dl = Local function declarations with default storage remain with default storage. *) let sto1 = - if local && sto = Storage_default && not isfun + if local && sto = Storage_default && not isfun then Storage_auto else sto in (* enter ident in environment with declared type, because @@ -2380,7 +2379,7 @@ let elab_KR_function_parameters env params defs loc = (* 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; + error loc' "declaration of '%s' which is not a function parameter" s; if ie <> NO_INIT then error loc' "illegal initialization of parameter '%s'" s; name @@ -2399,7 +2398,7 @@ let elab_KR_function_parameters env params defs loc = paramsenv | d -> (* Should never be produced by the parser *) fatal_error (Cabshelper.get_definitionloc d) - "Illegal declaration of function parameter" in + "illegal declaration of function parameter" in let kr_params_defs,paramsenv = let params,paramsenv = mmap elab_param_def env defs in List.concat params,paramsenv in @@ -2855,7 +2854,7 @@ let rec elab_stmt env ctx s = (print_typ env) b.etyp (print_typ env) ctx.ctx_return_typ else warning loc Unnamed - "incompatible conversion returning %a from a function with result type %a" + "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 diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll index cf8788c5..357c6c50 100644 --- a/cparser/Lexer.mll +++ b/cparser/Lexer.mll @@ -21,7 +21,7 @@ open Pre_parser_aux module SSet = Set.Make(String) let lexicon : (string, Cabs.cabsloc -> token) Hashtbl.t = Hashtbl.create 17 -let ignored_keyworkds : SSet.t ref = ref SSet.empty +let ignored_keywords : SSet.t ref = ref SSet.empty let () = List.iter (fun (key, builder) -> Hashtbl.add lexicon key builder) @@ -85,7 +85,7 @@ let () = ("while", fun loc -> WHILE loc)]; if Configuration.system <> "diab" then (* We can ignore the __extension__ GCC keyword. *) - ignored_keyworkds := SSet.add "__extension__" !ignored_keyworkds + ignored_keywords := SSet.add "__extension__" !ignored_keywords let init_ctx = SSet.singleton "__builtin_va_list" let types_context : SSet.t ref = ref init_ctx @@ -329,7 +329,7 @@ rule initial = parse | "," { COMMA(currentLoc lexbuf) } | "." { DOT(currentLoc lexbuf) } | identifier as id { - if SSet.mem id !ignored_keyworkds then + if SSet.mem id !ignored_keywords then initial lexbuf else try Hashtbl.find lexicon id (currentLoc lexbuf) diff --git a/cparser/Parse.ml b/cparser/Parse.ml index b2c83698..154e3dcf 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -69,7 +69,7 @@ let preprocessed_file transfs name sourcefile = | Parser.Parser.Inter.Fail_pr -> (* Theoretically impossible : implies inconsistencies between grammars. *) - Diagnostics.fatal_error Diagnostics.no_loc "Internal error while parsing" + Diagnostics.fatal_error Diagnostics.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/Unblock.ml b/cparser/Unblock.ml index 5df2e2cf..da8049a5 100644 --- a/cparser/Unblock.ml +++ b/cparser/Unblock.ml @@ -31,7 +31,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) - | _ -> Diagnostics.fatal_error Diagnostics.no_loc "Wrong type for array initializer" in + | _ -> Diagnostics.fatal_error Diagnostics.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/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml index 09694d0b..a45fff0c 100644 --- a/debug/DwarfPrinter.ml +++ b/debug/DwarfPrinter.ml @@ -241,7 +241,7 @@ module DwarfPrinter(Target: DWARF_TARGET): let abbrev = !curr_abbrev in incr curr_abbrev;abbrev - (* Mapping from abbreviation string to abbrevaiton id *) + (* Mapping from abbreviation string to abbreviaton id *) let abbrev_mapping: (string,int) Hashtbl.t = Hashtbl.create 7 (* Look up the id of the abbreviation and add it if it is missing *) diff --git a/driver/Assembler.mli b/driver/Assembler.mli index d8a4e32b..4f2e95ae 100644 --- a/driver/Assembler.mli +++ b/driver/Assembler.mli @@ -15,7 +15,7 @@ val assemble: string -> string -> unit (** From asm to object file *) val assembler_actions: (Commandline.pattern * Commandline.action) list - (** Commandline optins affecting the assembler *) + (** Commandline options affecting the assembler *) val assembler_help: string (** Commandline help description *) diff --git a/driver/Commandline.ml b/driver/Commandline.ml index f139212d..75ca1683 100644 --- a/driver/Commandline.ml +++ b/driver/Commandline.ml @@ -74,7 +74,7 @@ let parse_array spec argv first last = with Not_found -> find_action s inexact_cases in match optact with | None -> - let msg = sprintf "Unknown argument `%s'" s in + let msg = sprintf "unknown argument `%s'" s in raise (CmdError msg) | Some(Set r) -> r := true; parse (i+1) @@ -86,7 +86,7 @@ let parse_array spec argv first last = if i + 1 <= last then begin fn argv.(i+1); parse (i+2) end else begin - let msg = sprintf "Option `%s' expects an argument" s in + let msg = sprintf "option `%s' expects an argument" s in raise (CmdError msg) end | Some(Integer fn) -> @@ -95,19 +95,19 @@ let parse_array spec argv first last = try int_of_string argv.(i+1) with Failure _ -> - let msg = sprintf "Argument to option `%s' must be an integer" s in + let msg = sprintf "argument to option `%s' must be an integer" s in raise (CmdError msg) in fn n; parse (i+2) end else begin - let msg = sprintf "Option `%s' expects an argument" s in + let msg = sprintf "option `%s' expects an argument" s in raise (CmdError msg) end | Some (Ignore) -> if i + 1 <= last then begin parse (i+2) end else begin - let msg = sprintf "Option `%s' expects an argument" s in + let msg = sprintf "option `%s' expects an argument" s in raise (CmdError msg) end | Some (Unit f) -> f (); parse (i+1) @@ -131,7 +131,7 @@ let long_int_action key s = try int_of_string s with Failure _ -> - let msg = sprintf "Argument to option `%s' must be an integer" key in + let msg = sprintf "argument to option `%s' must be an integer" key in raise (CmdError msg) let longopt_int key f = diff --git a/driver/Driver.ml b/driver/Driver.ml index 0ad820ea..8ab8557c 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -404,7 +404,7 @@ let _ = parse_cmdline cmdline_actions; DebugInit.init (); (* Initialize the debug functions *) if nolink () && !option_o <> None && !num_source_files >= 2 then - fatal_error no_loc "Ambiguous '-o' option (multiple source files)"; + fatal_error no_loc "ambiguous '-o' option (multiple source files)"; if !num_input_files = 0 then fatal_error no_loc "no input file"; let linker_args = time "Total compilation time" perform_actions () in diff --git a/driver/Driveraux.ml b/driver/Driveraux.ml index ccc3d00d..5b2d792e 100644 --- a/driver/Driveraux.ml +++ b/driver/Driveraux.ml @@ -47,7 +47,7 @@ let command stdout args = match status with | Unix.WEXITED rc -> rc | Unix.WSIGNALED n | Unix.WSTOPPED n -> - error no_loc "Command '%s' killed on a signal." argv.(0); -1 + error no_loc "command '%s' killed on a signal." argv.(0); -1 with Unix.Unix_error(err, fn, param) -> error no_loc "executing '%s': %s: %s %s" argv.(0) fn (Unix.error_message err) param; diff --git a/driver/Frontend.mli b/driver/Frontend.mli index 39f0e612..a18c2704 100644 --- a/driver/Frontend.mli +++ b/driver/Frontend.mli @@ -18,7 +18,7 @@ val parse_c_file: string -> string -> Csyntax.coq_function Ctypes.program (** From preprocessed C to Csyntax *) val prepro_actions: (Commandline.pattern * Commandline.action) list - (** Commandline optins affecting the frontend *) + (** Commandline options affecting the frontend *) val prepro_help: string (** Commandline help description *) diff --git a/driver/Linker.mli b/driver/Linker.mli index 3b92da05..dd034543 100644 --- a/driver/Linker.mli +++ b/driver/Linker.mli @@ -12,10 +12,10 @@ (* *********************************************************************) val linker: string -> string list -> unit - (** Link files into executbale *) + (** Link files into executable *) val linker_actions: (Commandline.pattern * Commandline.action) list - (** Commandline optins affecting the assembler *) + (** Commandline options affecting the assembler *) val linker_help: string (** Commandline help description *) diff --git a/lib/Readconfig.mll b/lib/Readconfig.mll index e71c8fb7..7b98255e 100644 --- a/lib/Readconfig.mll +++ b/lib/Readconfig.mll @@ -43,9 +43,9 @@ let error msg lexbuf = lexbuf.lex_curr_p.pos_lnum, msg))) -let ill_formed_line lexbuf = error "Ill-formed line" lexbuf -let unterminated_quote lexbuf = error "Unterminated quote" lexbuf -let lone_backslash lexbuf = error "Lone \\ (backslash) at end of file" lexbuf +let ill_formed_line lexbuf = error "ill-formed line" lexbuf +let unterminated_quote lexbuf = error "unterminated quote" lexbuf +let lone_backslash lexbuf = error "lone \\ (backslash) at end of file" lexbuf } -- cgit