diff options
author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2018-02-08 16:38:54 +0100 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-02-08 16:38:54 +0100 |
commit | f02f00a01b598567f70e138c144d9581973802e6 (patch) | |
tree | db15b2ad60692f936435cdd784e7bb7f6a977a40 /driver/Driveraux.ml | |
parent | 54fa98c3833091a75d0c1afe84b42afc35452fe3 (diff) | |
download | compcert-f02f00a01b598567f70e138c144d9581973802e6.tar.gz compcert-f02f00a01b598567f70e138c144d9581973802e6.zip |
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.
Diffstat (limited to 'driver/Driveraux.ml')
-rw-r--r-- | driver/Driveraux.ml | 25 |
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 = |