package libsail

  1. Overview
  2. Docs

Module Libsail.ReportingSource

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.

Sourceval opt_warnings : bool ref

If this is false, Sail will never generate any warnings

Sourceval opt_all_warnings : bool ref

If this is true, we will print all warnings, even if generated with ~once_from.

Sourceval opt_backtrace_length : int ref

How many backtrace entries to show for unreachable code errors

Auxiliary Functions

Sourceval loc_to_string : Parse_ast.l -> string

loc_to_string prints a location as a string, including source code

Sourceval loc_file : Parse_ast.l -> string option

loc_file returns the file for a location

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

Reduce a location to a pair of positions if possible

Sourceval is_unknown_loc : Ast.l -> bool

Returns true if a loc is Unknown. In the case of Hint location only checks the base location.

Sourceval loc_range_to_src : Lexing.position -> Lexing.position -> string

loc_range_to_src returns the source code text of a range *

Adjust the range of a location. Note that only the primary location is adjusted. Hint locations are unaffected.

Sourceval short_loc_to_string : Parse_ast.l -> string

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

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

print_err prints a custom error message to stderr.

Sourceval start_loc : Parse_ast.l -> Parse_ast.l

Reduce all spans in a location to just their starting characters

The error type

Sourcetype 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 * 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 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 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.

Sourceexception Fatal_error of error
Sourceval err_todo : Parse_ast.l -> string -> exn
Sourceval err_general : Parse_ast.l -> string -> exn
Sourceval err_unreachable : Parse_ast.l -> (string * int * int * int) -> string -> exn
Sourceval err_typ : ?hint:string -> Parse_ast.l -> string -> exn
Sourceval err_syntax : Lexing.position -> string -> exn
Sourceval err_syntax_loc : Parse_ast.l -> string -> exn
Sourceval err_lex : Lexing.position -> string -> exn
Sourceval 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.

Sourceval 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.

Sourceval print_type_error : ?hint:string -> Parse_ast.l -> string -> unit
Sourceval 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

Sourceval warn : ?once_from:(string * int * int * int) -> ?force_show:bool -> string -> Parse_ast.l -> string -> unit

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

Sourceval format_warn : ?once_from:(string * int * int * int) -> string -> Parse_ast.l -> Error_format.message -> unit
Sourceval suppressed_warning_info : unit -> unit

Print information about suppressed warnings

Sourceval simple_warn : string -> unit

Print a simple one-line warning without a location.

Sourceval 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

Sourceval get_sail_dir : string -> string
Sourceval system_checked : ?loc:Parse_ast.l -> string -> unit

Run a command using Unix.system, but raise a Reporting exception if the command fails or is stopped/killed by a signal

Sourcemodule Position : sig ... end