Module AltErgoLib.Errors

Errors module

This module aims to regroup all exception that can be raised by the Alt-Ergo-lib

Error types

type typing_error =
  1. | NonPositiveBitvType of int
  2. | ThExtError of string
  3. | ThSemTriggerError

Error that can be raised by the typechecker

type run_error =
  1. | Invalid_steps_count of int
  2. | Failed_check_unsat_core
  3. | Unsupported_feature of string
  4. | Stack_underflow

Errors that can be raised at solving

type mode_error =
  1. | Invalid_set_option of string
  2. | Forbidden_command of string

Errors raised when performing actions forbidden in some modes.

type model_error =
  1. | Subst_type_clash of Id.t * Ty.t * Ty.t
  2. | Subst_not_model_term of Expr.t

Errors raised while using models.

type error =
  1. | Typing_error of Dolmen.Std.Loc.loc * typing_error
    (*

    Error used at typing

    *)
  2. | Run_error of run_error
    (*

    Error used during solving

    *)
  3. | Warning_as_error
  4. | Dolmen_error of int * string
    (*

    Error code + description raised by dolmen.

    *)
  5. | Mode_error of Util.mode * mode_error
    (*

    Error used when performing actions forbidden in some modes.

    *)
  6. | Model_error of model_error
    (*

    Error raised while using models.

    *)

All types of error that can be raised

Exceptions

exception Error of error

Raising exceptions functions

val error : error -> 'a

Raise the input error as Error

val typing_error : typing_error -> Dolmen.Std.Loc.loc -> 'a

Raise the input typing_error as Typing_error

val run_error : run_error -> 'a

Raise the input run_error as Run_error

val warning_as_error : unit -> unit

Raise Warning_as_error as Error if the option warning-as-error is set This function can be use after warning

val invalid_set_option : Util.mode -> string -> 'a

Raise Mode_error (Invalid_set_option str) as Error if an option is being set when it should be immutable.

val forbidden_command : Util.mode -> string -> 'a

Raise Mode_error (Forbidden_command str) as Error if a command is being used in a mode where it should not be available.

Printing

val report : Stdlib.Format.formatter -> error -> unit

Print a message on the formatter corresponding to the error