From f02f00a01b598567f70e138c144d9581973802e6 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 8 Feb 2018 16:38:54 +0100 Subject: 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. --- cparser/Diagnostics.mli | 86 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 86 insertions(+) create mode 100644 cparser/Diagnostics.mli (limited to 'cparser/Diagnostics.mli') diff --git a/cparser/Diagnostics.mli b/cparser/Diagnostics.mli new file mode 100644 index 00000000..54395136 --- /dev/null +++ b/cparser/Diagnostics.mli @@ -0,0 +1,86 @@ +(* *********************************************************************) +(* *) +(* 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 -> unit + (** Check whether errors occured and raise abort if an error 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 *) + +val no_loc : string * int +(** Location used for unknown locations *) + +val file_loc : string -> string * int +(** [file_loc f] generates a location for file [f] *) -- cgit