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/Frontend.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/Frontend.ml')
-rw-r--r-- | driver/Frontend.ml | 15 |
1 files changed, 3 insertions, 12 deletions
diff --git a/driver/Frontend.ml b/driver/Frontend.ml index 2b9d5860..2bc4f844 100644 --- a/driver/Frontend.ml +++ b/driver/Frontend.ml @@ -14,7 +14,6 @@ open Clflags open Commandline open Driveraux -open Printf (* Common frontend functions between clightgen and ccomp *) @@ -22,6 +21,7 @@ open Printf (* From C to preprocessed C *) let preprocess ifile ofile = + Diagnostics.raise_on_errors (); let output = if ofile = "-" then None else Some ofile in let cmd = List.concat [ @@ -37,8 +37,6 @@ let preprocess ifile ofile = if exc <> 0 then begin if ofile <> "-" then safe_remove ofile; command_error "preprocessor" exc; - eprintf "Error during preprocessing.\n"; - exit 2 end (* From preprocessed C to Csyntax *) @@ -54,18 +52,11 @@ let parse_c_file sourcename ifile = ^ (if !option_fpacked_structs then "p" else "") in (* Parsing and production of a simplified C AST *) - let ast = - match Parse.preprocessed_file simplifs sourcename ifile with - | None -> exit 2 - | Some p -> p in + let ast = Parse.preprocessed_file simplifs sourcename ifile in (* Save C AST if requested *) Cprint.print_if ast; (* Conversion to Csyntax *) - let csyntax = - match Timing.time "CompCert C generation" C2C.convertProgram ast with - | None -> exit 2 - | Some p -> p in - flush stderr; + let csyntax = Timing.time "CompCert C generation" C2C.convertProgram ast in (* Save CompCert C AST if requested *) PrintCsyntax.print_if csyntax; csyntax |