package libsail

  1. Overview
  2. Docs
package libsail
Legend:
Library
Module
Module type
Parameter
Class
Class type

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 Stdlib.ref

If this is false, Sail will never generate any warnings

val opt_backtrace_length : int Stdlib.ref

How many backtrace entries to show for unreachable code errors

Auxiliary Functions

val loc_to_string : Parse_ast.l -> string

loc_to_string prints a location as a string, including source code

val loc_file : Parse_ast.l -> string option

loc_file returns the file for a location

val simp_loc : Ast.l -> (Stdlib.Lexing.position * Stdlib.Lexing.position) option

Reduce a location to a pair of positions if possible

val short_loc_to_string : Parse_ast.l -> string

short_loc_to_string prints the location as a single line in a simple format

val print_err : Parse_ast.l -> string -> string -> unit

print_err prints a custom error message to stderr.

val start_loc : Parse_ast.l -> Parse_ast.l

Reduce all spans in a location to just their starting characters

The error type

type error = private
  1. | Err_general of Parse_ast.l * string
    (*

    General errors, used for multi purpose. If you are unsure, use this one.

    *)
  2. | Err_unreachable of Parse_ast.l * string * int * int * int * Stdlib.Printexc.raw_backtrace * string
    (*

    Unreachable errors should never be thrown. They represent an internal Sail error.

    *)
  3. | Err_todo of Parse_ast.l * string
    (*

    Err_todo indicates that some feature is unimplemented.

    *)
  4. | Err_syntax of Stdlib.Lexing.position * string
  5. | Err_syntax_loc of Parse_ast.l * string
    (*

    Err_syntax and Err_syntax_loc are used for syntax errors by the parser.

    *)
  6. | Err_lex of Stdlib.Lexing.position * string
    (*

    Err_lex is a lexical error generated by the lexer.

    *)
  7. | Err_type of Parse_ast.l * string option * string
    (*

    Err_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 error
val err_todo : Parse_ast.l -> string -> exn
val err_general : Parse_ast.l -> string -> exn
val err_unreachable : Parse_ast.l -> (string * int * int * int) -> string -> exn
val err_typ : ?hint:string -> Parse_ast.l -> string -> exn
val err_syntax : Stdlib.Lexing.position -> string -> exn
val err_syntax_loc : Parse_ast.l -> string -> exn
val err_lex : Stdlib.Lexing.position -> string -> exn
val unreachable : Parse_ast.l -> (string * int * int * int) -> string -> 'a

Raise 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 -> unit

Print an error to stdout.

  • parameter interactive

    If this is true (default false) then unreachable errors are reported as general errors. This is used by the interactive read-eval-print loop. The interactive mode exposes a lot of internal features, so it's possible to excute code paths from the interactive mode that would otherwise be unreachable during normal execution.

val forbid_errors : (string * int * int * int) -> ('a -> 'b) -> 'a -> 'b

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 -> unit

Print a warning message. The first string is printed before the location, the second after.

val simple_warn : string -> unit

Print a simple one-line warning without a location.

val suppress_warnings_for_file : string -> unit

Will suppress all warnings for a given (Sail) file name. Used by $suppress_warnings directive in process_file.ml

val get_sail_dir : string -> string