summaryrefslogtreecommitdiff
path: root/src/reporting.mli
diff options
context:
space:
mode:
authorAlasdair Armstrong2018-10-31 15:43:56 +0000
committerAlasdair Armstrong2018-10-31 15:43:56 +0000
commit001e28b487c8a4cb2a25519a3acc8ac8c1aaabf5 (patch)
treec50d5a7bb026e875db96af53fd44d58387d7a7c6 /src/reporting.mli
parent5298e209f0ae12e51f3050888e18ad9be09543e4 (diff)
Rename Reporting_basic to Reporting
There is no Reporting_complex, so it's not clear what the basic is intended to signify anyway. Add a GitHub issue link to any err_unreachable errors (as they are all bugs)
Diffstat (limited to 'src/reporting.mli')
-rw-r--r--src/reporting.mli115
1 files changed, 115 insertions, 0 deletions
diff --git a/src/reporting.mli b/src/reporting.mli
new file mode 100644
index 00000000..a6878d6a
--- /dev/null
+++ b/src/reporting.mli
@@ -0,0 +1,115 @@
+(**************************************************************************)
+(* Sail *)
+(* *)
+(* Copyright (c) 2013-2017 *)
+(* Kathyrn Gray *)
+(* Shaked Flur *)
+(* Stephen Kell *)
+(* Gabriel Kerneis *)
+(* Robert Norton-Wright *)
+(* Christopher Pulte *)
+(* Peter Sewell *)
+(* Alasdair Armstrong *)
+(* Brian Campbell *)
+(* Thomas Bauereiss *)
+(* Anthony Fox *)
+(* Jon French *)
+(* Dominic Mulligan *)
+(* Stephen Kell *)
+(* Mark Wassell *)
+(* *)
+(* All rights reserved. *)
+(* *)
+(* This software was developed by the University of Cambridge Computer *)
+(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *)
+(* (REMS) project, funded by EPSRC grant EP/K008528/1. *)
+(* *)
+(* Redistribution and use in source and binary forms, with or without *)
+(* modification, are permitted provided that the following conditions *)
+(* are met: *)
+(* 1. Redistributions of source code must retain the above copyright *)
+(* notice, this list of conditions and the following disclaimer. *)
+(* 2. Redistributions in binary form must reproduce the above copyright *)
+(* notice, this list of conditions and the following disclaimer in *)
+(* the documentation and/or other materials provided with the *)
+(* distribution. *)
+(* *)
+(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *)
+(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *)
+(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *)
+(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *)
+(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *)
+(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *)
+(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *)
+(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *)
+(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *)
+(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *)
+(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *)
+(* SUCH DAMAGE. *)
+(**************************************************************************)
+
+(** Basic error reporting
+
+ [Reporting] contains functions to report errors and warnings.
+ It contains functions to print locations ([Parse_ast.l] and [Ast.l]) and lexing positions.
+
+ The main functionality is reporting errors. This is done by raising a
+ [Fatal_error] exception. This is caught internally and reported via [report_error].
+ There are several predefined types of errors which all cause different error
+ messages. If none of these fit, [Err_general] can be used.
+
+*)
+
+(** {2 Auxiliary Functions } *)
+
+val loc_to_string : Parse_ast.l -> string
+
+(** [print_err fatal print_loc_source l head mes] prints an error / warning message to
+ std-err. It starts with printing location information stored in [l]
+ It then prints "head: mes". If [fatal] is set, the program exists with error-code 1 afterwards.
+*)
+val print_err : bool -> bool -> Parse_ast.l -> string -> string -> unit
+
+(** {2 Errors } *)
+
+(** Errors stop execution and print a message; they typically have a location and message.
+*)
+type error =
+ (** General errors, used for multi purpose. If you are unsure, use this one. *)
+ | Err_general of Parse_ast.l * string
+
+ (** Unreachable errors should never be thrown. It means that some
+ code was excuted that the programmer thought of as unreachable *)
+ | Err_unreachable of Parse_ast.l * (string * int * int * int) * string
+
+ (** [Err_todo] indicates that some feature is unimplemented; it should be built using [err_todo]. *)
+ | Err_todo of Parse_ast.l * string
+
+ | Err_syntax of Lexing.position * string
+ | Err_syntax_locn of Parse_ast.l * string
+ | Err_lex of Lexing.position * string
+ | Err_type of Parse_ast.l * string
+ | Err_type_dual of Parse_ast.l * Parse_ast.l * string
+
+exception Fatal_error of error
+
+(** [err_todo l m] is an abreviatiation for [Fatal_error (Err_todo (l, m))] *)
+val err_todo : Parse_ast.l -> string -> exn
+
+(** [err_general l m] is an abreviatiation for [Fatal_error (Err_general (b, l, m))] *)
+val err_general : Parse_ast.l -> string -> exn
+
+(** [err_unreachable l __POS__ m] is an abreviatiation for [Fatal_error (Err_unreachable (l, __POS__, m))] *)
+val err_unreachable : Parse_ast.l -> (string * int * int * int) -> string -> exn
+
+(** [err_typ l m] is an abreviatiation for [Fatal_error (Err_type (l, m))] *)
+val err_typ : Parse_ast.l -> string -> exn
+
+(** [err_typ_dual l1 l2 m] is an abreviatiation for [Fatal_error (Err_type_dual (l1, l2, m))] *)
+val err_typ_dual : Parse_ast.l -> Parse_ast.l -> string -> exn
+
+(** Report error should only be used by main to print the error in the end. Everywhere else,
+ raising a [Fatal_error] exception is recommended. *)
+val report_error : error -> 'a
+
+val print_error : error -> unit