Sail 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.
val opt_warnings : bool refIf this is false, Sail will never generate any warnings
val opt_backtrace_length : int refHow many backtrace entries to show for unreachable code errors
val loc_to_string : Parse_ast.l -> stringloc_to_string prints a location as a string, including source code
val loc_file : Parse_ast.l -> string optionloc_file returns the file for a location
val simp_loc : Ast.l -> (Lexing.position * Lexing.position) optionReduce a location to a pair of positions if possible
val short_loc_to_string : Parse_ast.l -> stringshort_loc_to_string prints the location as a single line in a simple format
val print_err : Parse_ast.l -> string -> string -> unitprint_err prints a custom error message to stderr.
val start_loc : Parse_ast.l -> Parse_ast.lReduce all spans in a location to just their starting characters
type error = private | Err_general of Parse_ast.l * stringGeneral errors, used for multi purpose. If you are unsure, use this one.
*)| Err_unreachable of Parse_ast.l
* string * int * int * int
* Printexc.raw_backtrace
* stringUnreachable errors should never be thrown. They represent an internal Sail error.
*)| Err_todo of Parse_ast.l * stringErr_todo indicates that some feature is unimplemented.
| Err_syntax of Lexing.position * string| Err_syntax_loc of Parse_ast.l * stringErr_syntax and Err_syntax_loc are used for syntax errors by the parser.
| Err_lex of Lexing.position * stringErr_lex is a lexical error generated by the lexer.
| Err_type of Parse_ast.l * string option * stringErr_type is a type error. See the Type_error module.
Errors stop execution and print a message; they typically have a location and message.
Note that all these errors are intended to be fatal, so should not be caught other than by the top-level function.
exception Fatal_error of errorval err_todo : Parse_ast.l -> string -> exnval err_general : Parse_ast.l -> string -> exnval err_unreachable :
Parse_ast.l ->
(string * int * int * int) ->
string ->
exnval err_typ : ?hint:string -> Parse_ast.l -> string -> exnval err_syntax : Lexing.position -> string -> exnval err_syntax_loc : Parse_ast.l -> string -> exnval err_lex : Lexing.position -> string -> exnval unreachable : Parse_ast.l -> (string * int * int * int) -> string -> 'aRaise an unreachable exception.
This should always be used over an assert false or a generic OCaml failwith exception when appropriate
val print_error : ?interactive:bool -> error -> unitPrint an error to stdout.
This function transforms all errors raised by the provided function into internal Err_unreachable errors
val warn :
?once_from:(string * int * int * int) ->
string ->
Parse_ast.l ->
string ->
unitPrint a warning message. The first string is printed before the location, the second after.
val format_warn :
?once_from:(string * int * int * int) ->
string ->
Parse_ast.l ->
Error_format.message ->
unitWill suppress all warnings for a given (Sail) file name. Used by $suppress_warnings directive in process_file.ml