package libsail

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Auxiliary Functions
The error type

libsail
- Libsail
  - Anf
  - Ast
  - Ast_defs
  - Ast_util
    
    Bindings
    
    Id
    
    IdSet
    
    KBindings
    
    KOpt
    
    KOptMap
    
    KOptSet
    
    Kid
    
    KidSet
    
    Kind
    
    NC
    
    NCMap
    
    Nexp
    
    NexpMap
    
    NexpSet
    
    Typ
    
    TypMap
  - Bitfield
  - Callgraph
    
    G
    
    Node
  - Constant_fold
    
    StringMap
  - Constant_propagation
  - Constant_propagation_mutrec
  - Constraint
  - Effects
    
    EffectSet
  - Elf_loader
  - Error_format
  - Frontend
  - Graph
    
    Make
    
    Ord
    
    OrderedType
    
    S
  - Initial_check
  - Interactive
  - Interpreter
  - Jib
  - Jib_compile
    
    Config
    
    Make
    
    C
  - Jib_optimize
  - Jib_util
    
    CT
    
    CTList
    
    CTListSet
    
    CTMap
    
    CTSet
    
    Name
    
    NameCT
    
    NameCTMap
    
    NameCTSet
    
    NameMap
    
    NameSet
    
    UBindings
    
    UId
  - Lexer
    
    M
  - Libsail_sites
    
    Sites
  - Monomorphise
  - Nl_flow
  - Optimize
  - Outcome_rewrites
  - Parse_ast
  - Parser
  - Parser_combinators
  - Pattern_completeness
    
    Config
    
    Make
    
    C
  - Preprocess
  - Pretty_print_common
  - Pretty_print_sail
  - Profile
  - Property
    
    Event
  - Reporting
  - Rewriter
  - Rewrites
  - Sail2_instr_kinds
  - Sail2_operators
  - Sail2_operators_bitlists
  - Sail2_prompt
  - Sail2_prompt_monad
  - Sail2_values
  - Sail_lib
    
    BitType
    
    Mem
  - Scattered
  - Spec_analysis
  - Specialize
  - Splice
  - State
  - Target
  - Type_check
    
    Env
  - Type_error
  - Util
    
    Duplicate
    
    S
    
    IntIntSet
    
    IntSet
  - Value
    
    StringMap
  - Value2

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 ref

If this is false, Sail will never generate any warnings

val opt_backtrace_length : int 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 -> (Lexing.position * 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

| Err_general of Parse_ast.l * string
(*
General 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 * string
(*
Unreachable errors should never be thrown. They represent an internal Sail error.
*)
| Err_todo of Parse_ast.l * string
(*
Err_todo indicates that some feature is unimplemented.
*)
| Err_syntax of Lexing.position * string
| Err_syntax_loc of Parse_ast.l * string
(*
Err_syntax and Err_syntax_loc are used for syntax errors by the parser.
*)
| Err_lex of Lexing.position * string
(*
Err_lex is a lexical error generated by the lexer.
*)
| 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 : Lexing.position -> string -> exn

val err_syntax_loc : Parse_ast.l -> string -> exn

val err_lex : 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