Refactor the handling of errors and warnings (#44)

* Module Cerrors is now called Diagnostic and can be used in parts of CompCert other than cparser/

* Replaced eprintf error.  Instead of having eprintf msg; exit 2 use the functions from the
Diagnostics module.

* Raise on error before calling external tools.

* Added diagnostics to clightgen.

* Fix error handling of AsmToJson.

* Cleanup error handling of Elab and C2C.

*The implementation of location printing (file & line) is simplified and correctly prints valid filenames with invalid lines.

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') =