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 /powerpc | |
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 'powerpc')
-rw-r--r-- | powerpc/AsmToJSON.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index 5baed5dc..7c4c8f8a 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -340,7 +340,7 @@ let pp_instructions pp ic = begin match ef with | EF_inline_asm _ -> instruction pp "Pinlineasm" [Id]; - Cerrors.warning ("",-10) Cerrors.Inline_asm_sdump "inline assembler is not supported in sdump" + Diagnostics.(warning no_loc Inline_asm_sdump "inline assembler is not supported in sdump") | EF_annot (kind,txt,targs) -> let annot_string = PrintAsmaux.annot_text preg_annot "r1" (camlstring_of_coqstring txt) args in let len = String.length annot_string in |