diff options
Diffstat (limited to 'cparser')
-rw-r--r-- | cparser/Bitfields.ml | 2 | ||||
-rw-r--r-- | cparser/Checks.ml | 2 | ||||
-rw-r--r-- | cparser/Cutil.ml | 2 | ||||
-rw-r--r-- | cparser/Diagnostics.ml (renamed from cparser/Cerrors.ml) | 19 | ||||
-rw-r--r-- | cparser/Diagnostics.mli (renamed from cparser/Cerrors.mli) | 10 | ||||
-rw-r--r-- | cparser/Elab.ml | 4 | ||||
-rw-r--r-- | cparser/ExtendedAsm.ml | 4 | ||||
-rw-r--r-- | cparser/Lexer.mll | 10 | ||||
-rw-r--r-- | cparser/PackedStructs.ml | 2 | ||||
-rw-r--r-- | cparser/Parse.ml | 15 | ||||
-rw-r--r-- | cparser/Parse.mli | 2 | ||||
-rw-r--r-- | cparser/Rename.ml | 2 | ||||
-rw-r--r-- | cparser/Unblock.ml | 3 |
13 files changed, 43 insertions, 34 deletions
diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml index 35da5d4e..e0dccbd2 100644 --- a/cparser/Bitfields.ml +++ b/cparser/Bitfields.ml @@ -66,7 +66,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 + Diagnostics.warning Diagnostics.no_loc Diagnostics.Unnamed "not all values of type 'enum %s' can be represented in bit-field '%s' of struct '%s' (%d bits are not enough)" eid.C.name fld sid.C.name n; false diff --git a/cparser/Checks.ml b/cparser/Checks.ml index 073d1057..ee36e226 100644 --- a/cparser/Checks.ml +++ b/cparser/Checks.ml @@ -14,7 +14,7 @@ (* *********************************************************************) open C -open Cerrors +open Diagnostics open Cutil open Env diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index 9bc11141..71c253f8 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -15,7 +15,7 @@ (* Operations on C types and abstract syntax *) -open Cerrors +open Diagnostics open C open Env open Machine diff --git a/cparser/Cerrors.ml b/cparser/Diagnostics.ml index 34fc4fcf..d9b96393 100644 --- a/cparser/Cerrors.ml +++ b/cparser/Diagnostics.ml @@ -299,11 +299,13 @@ let parse_loc_format s = (* Print the location or ccomp for the case of unknown loc *) let pp_loc fmt (filename,lineno) = - if filename <> "" && lineno <> -10 && filename <> "cabs loc unknown" then + let lineno = if lineno = -10 then "" else match !diagnostics_format with - | Default -> fprintf fmt "%t%s:%d:%t " bc filename lineno rsc - | MSVC -> fprintf fmt "%t%s(%d):%t " bc filename lineno rsc - | Vi -> fprintf fmt "%t%s +%d:%t " bc filename lineno rsc + | Default -> sprintf ":%d" lineno + | MSVC -> sprintf "(%d)" lineno + | Vi -> sprintf " +%d" lineno in + if filename <> "" && filename <> "cabs loc unknown" then + fprintf fmt "%t%s%s:%t " bc filename lineno rsc else fprintf fmt "%tccomp:%t " bc rsc @@ -341,11 +343,12 @@ let fatal_error loc fmt = fatal_error None loc fmt let check_errors () = - if !num_errors > 0 then + if !num_errors > 0 then begin eprintf "@[<hov 0>%d error%s detected.@]@." !num_errors (if !num_errors = 1 then "" else "s"); - !num_errors > 0 + raise Abort + end let error_option w = let key = string_of_warning w in @@ -428,3 +431,7 @@ let crash exn = eprintf "Fatal error: uncaught exception %s\n%s" exc backtrace; exit 2 end + +let no_loc = ("", -1) + +let file_loc file = (file,-10) diff --git a/cparser/Cerrors.mli b/cparser/Diagnostics.mli index c351443c..54395136 100644 --- a/cparser/Cerrors.mli +++ b/cparser/Diagnostics.mli @@ -21,8 +21,8 @@ val reset : unit -> unit exception Abort (** Exception raised upon fatal errors *) -val check_errors : unit -> bool - (** Check whether errors occured *) +val check_errors : unit -> unit + (** Check whether errors occured and raise abort if an error occured *) type warning_type = | Unnamed (** warnings which cannot be turned off *) @@ -78,3 +78,9 @@ val raise_on_errors : unit -> unit val crash: exn -> unit (** Report the backtrace of the last exception and exit *) + +val no_loc : string * int +(** Location used for unknown locations *) + +val file_loc : string -> string * int +(** [file_loc f] generates a location for file [f] *) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 86e71865..4de43fe0 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -20,8 +20,8 @@ open Machine open Cabs open C -open Cerrors -open Cutil +open Diagnostics +open !Cutil (** * Utility functions *) diff --git a/cparser/ExtendedAsm.ml b/cparser/ExtendedAsm.ml index 30d1a0cc..6cd95aec 100644 --- a/cparser/ExtendedAsm.ml +++ b/cparser/ExtendedAsm.ml @@ -33,7 +33,7 @@ open Printf open Machine open C open Cutil -open Cerrors +open Diagnostics (* Renaming of labeled and numbered operands *) @@ -176,7 +176,7 @@ let rename_placeholders loc template subst = try StringMap.find p subst with Not_found -> - error loc"'%s' in asm text does not designate any operand" p; + error loc "'%s' in asm text does not designate any operand" p; "%<error>" in Str.global_substitute re_asm_placeholder diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll index ec344f7a..cf8788c5 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 + Diagnostics.fatal_error (lb.lex_curr_p.pos_fname,lb.lex_curr_p.pos_lnum) fmt let error lb fmt = - Cerrors.error + Diagnostics.error (lb.lex_curr_p.pos_fname,lb.lex_curr_p.pos_lnum) fmt let warning lb fmt = - Cerrors.warning - (lb.lex_curr_p.pos_fname,lb.lex_curr_p.pos_lnum) Cerrors.Unnamed ("warning: " ^^ fmt) + Diagnostics.warning + (lb.lex_curr_p.pos_fname,lb.lex_curr_p.pos_lnum) Diagnostics.Unnamed ("warning: " ^^ fmt) (* Simple character escapes *) @@ -483,7 +483,7 @@ and singleline_comment = parse and supplier = I.lexer_lexbuf_to_supplier lexer lexbuf and succeed () = () and fail checkpoint = - Cerrors.fatal_error_raw "%s" (ErrorReports.report text !buffer checkpoint) + Diagnostics.fatal_error_raw "%s" (ErrorReports.report text !buffer checkpoint) in I.loop_handle succeed fail supplier checkpoint diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml index b74a29d4..e1287eb8 100644 --- a/cparser/PackedStructs.ml +++ b/cparser/PackedStructs.ml @@ -23,7 +23,7 @@ open Machine open C open Cutil open Env -open Cerrors +open Diagnostics open Transform (* The set of struct fields that are byte-swapped. diff --git a/cparser/Parse.ml b/cparser/Parse.ml index ecd13332..8665e158 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -46,7 +46,7 @@ let read_file sourcefile = text let preprocessed_file transfs name sourcefile = - Cerrors.reset(); + Diagnostics.reset(); (* Reading the whole file at once may seem costly, but seems to be the simplest / most robust way of accessing the text underlying a range of positions. This is used when printing an error message. @@ -55,7 +55,6 @@ let preprocessed_file transfs name sourcefile = on my machine. *) let text = read_file sourcefile in let p = - try let t = parse_transformations transfs in let rec inf = Datatypes.S inf in let ast : Cabs.definition list = @@ -70,13 +69,11 @@ let preprocessed_file transfs name sourcefile = | Parser.Parser.Inter.Fail_pr -> (* Theoretically impossible : implies inconsistencies between grammars. *) - Cerrors.fatal_error Cutil.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 - Cerrors.raise_on_errors (); - Timing.time2 "Emulations" transform_program t p1 name - with - | Cerrors.Abort -> - [] in - if Cerrors.check_errors() then None else Some p + Diagnostics.check_errors (); + Timing.time2 "Emulations" transform_program t p1 name in + Diagnostics.check_errors(); + p diff --git a/cparser/Parse.mli b/cparser/Parse.mli index 58c3cfb9..433e2e73 100644 --- a/cparser/Parse.mli +++ b/cparser/Parse.mli @@ -15,7 +15,7 @@ (* Entry point for the library: parse, elaborate, and transform *) -val preprocessed_file: string -> string -> string -> C.program option +val preprocessed_file: string -> string -> string -> C.program (* first arg: desired transformations second arg: source file name before preprocessing diff --git a/cparser/Rename.ml b/cparser/Rename.ml index f402ea39..cdb5751e 100644 --- a/cparser/Rename.ml +++ b/cparser/Rename.ml @@ -83,7 +83,7 @@ let ident env id = try IdentMap.find id env.re_id with Not_found -> - Cerrors.fatal_error no_loc "internal error: rename: %s__%d unbound" + Diagnostics.fatal_error Diagnostics.no_loc "internal error: rename: %s__%d unbound" id.name id.stamp let rec typ env = function diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml index 91e2ce20..5df2e2cf 100644 --- a/cparser/Unblock.ml +++ b/cparser/Unblock.ml @@ -20,7 +20,6 @@ open C open Cutil -open Cerrors (* Convert an initializer to a list of assignment expressions. *) @@ -32,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) - | _ -> fatal_error 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') = |