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 /cparser/Cerrors.mli | |
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 'cparser/Cerrors.mli')
-rw-r--r-- | cparser/Cerrors.mli | 80 |
1 files changed, 0 insertions, 80 deletions
diff --git a/cparser/Cerrors.mli b/cparser/Cerrors.mli deleted file mode 100644 index c351443c..00000000 --- a/cparser/Cerrors.mli +++ /dev/null @@ -1,80 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(* Printing of warnings and error messages *) - -val reset : unit -> unit - (** Reset the error counters. *) - -exception Abort - (** Exception raised upon fatal errors *) - -val check_errors : unit -> bool - (** Check whether errors occured *) - -type warning_type = - | Unnamed (** warnings which cannot be turned off *) - | Unknown_attribute (** usage of unsupported/unknown attributes *) - | Zero_length_array (** gnu extension for zero lenght arrays *) - | Celeven_extension (** C11 features *) - | Gnu_empty_struct (** gnu extension for empty struct *) - | Missing_declarations (** declation which do not declare anything *) - | Constant_conversion (** dangerous constant conversions *) - | Int_conversion (** pointer <-> int conversions *) - | Varargs (** promotable vararg argument *) - | Implicit_function_declaration (** deprecated implicit function declaration *) - | Pointer_type_mismatch (** pointer type mismatch in ?: operator *) - | Compare_distinct_pointer_types (** comparison between different pointer types *) - | Implicit_int (** implict int parameter or return type *) - | Main_return_type (** wrong return type for main *) - | Invalid_noreturn (** noreturn function containing return *) - | Return_type (** void return in non-void function *) - | Literal_range (** literal ranges *) - | Unknown_pragmas (** unknown/unsupported pragma *) - | CompCert_conformance (** features that are not part of the CompCert C core language *) - | Inline_asm_sdump (** inline assembler used in combination of sdump *) - | Unused_variable (** unused local variables *) - | Unused_parameter (** unused function parameter *) - -val warning : (string * int) -> warning_type -> ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a -(** [warning (f,c) w fmt arg1 ... argN] formats the arguments [arg1] to [argN] as warining according to - the format string [fmt] and outputs the result on [stderr] with additional file [f] and column [c] - and warning key for [w] *) - -val error : (string * int) -> ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a -(** [error (f,c) w fmt arg1 ... argN] formats the arguments [arg1] to [argN] as error according to - the format string [fmt] and outputs the result on [stderr] with additional file [f] and column [c] - and warning key for [w]. *) - -val fatal_error : (string * int) -> ('a, Format.formatter, unit, unit, unit, 'b) format6 -> 'a -(** [fatal_error (f,c) w fmt arg1 ... argN] formats the arguments [arg1] to [argN] as error according to - the format string [fmt] and outputs the result on [stderr] with additional file [f] and column [c] - and warning key for [w]. Additionally raises the excpetion [Abort] after printing the error message *) - -val fatal_error_raw : ('a, out_channel, unit, 'b) format4 -> 'a -(** [fatal_error_raw] is identical to fatal_error, except it uses [Printf] and does not automatically - introduce indentation *) - -val warning_help : string -(** Help string for all warning options *) - -val warning_options : (Commandline.pattern * Commandline.action) list -(** List of all options for diagnostics *) - -val raise_on_errors : unit -> unit -(** Raise [Abort] if an error was encountered *) - -val crash: exn -> unit -(** Report the backtrace of the last exception and exit *) |