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.

1 files changed, 12 insertions, 13 deletions

diff --git a/driver/Driveraux.ml b/driver/Driveraux.ml
index 6d8d0adc..ccc3d00d 100644
--- a/driver/Driveraux.ml
+++ b/driver/Driveraux.ml
@@ -13,6 +13,7 @@
 
 open Printf
 open Clflags
+open Diagnostics
 
 (* Safe removal of files *)
 let safe_remove file =
@@ -46,9 +47,9 @@ let command stdout args =
     match status with
     | Unix.WEXITED rc -> rc
     | Unix.WSIGNALED n | Unix.WSTOPPED n ->
-        eprintf "Command '%s' killed on a signal.\n" argv.(0); -1
+        error no_loc "Command '%s' killed on a signal." argv.(0); -1
   with Unix.Unix_error(err, fn, param) ->
-    eprintf "Error executing '%s': %s: %s %s\n"
+    error no_loc "executing '%s': %s: %s %s"
             argv.(0) fn (Unix.error_message err) param;
     -1
 
@@ -81,7 +82,7 @@ let command ?stdout args =
     command stdout args
 
 let command_error n exc =
-  eprintf "Error: %s command failed with exit code %d (use -v to see invocation)\n" n exc
+  fatal_error no_loc "%s command failed with exit code %d (use -v to see invocation)\n" n exc
 
 
 (* Determine names for output files.  We use -o option if specified
@@ -105,20 +106,18 @@ let output_filename_default default_file =
 (* All input files should exist *)
 
 let ensure_inputfile_exists name =
-  if not (Sys.file_exists name) then begin
-    eprintf "error: no such file or directory: '%s'\n" name;
-    exit 2
-  end
+  if not (Sys.file_exists name) then
+    fatal_error no_loc "no such file or directory: '%s'" name
+
 (* Printing of error messages *)
 
-let print_error oc msg =
+let print_error pp msg =
   let print_one_error = function
-  | Errors.MSG s -> output_string oc (Camlcoq.camlstring_of_coqstring s)
-  | Errors.CTX i -> output_string oc (Camlcoq.extern_atom i)
-  | Errors.POS i -> fprintf oc "%ld" (Camlcoq.P.to_int32 i)
+  | Errors.MSG s -> Format.pp_print_string pp (Camlcoq.camlstring_of_coqstring s)
+  | Errors.CTX i -> Format.pp_print_string pp (Camlcoq.extern_atom i)
+  | Errors.POS i -> Format.fprintf pp "%ld" (Camlcoq.P.to_int32 i)
   in
-    List.iter print_one_error msg;
-    output_char oc '\n'
+  List.iter print_one_error msg
 
 (* Command-line parsing *)
 let explode_comma_option s =