This module aims to regroup all exception that can be raised by the Alt-Ergo-lib
type typing_error = | BitvExtract of int * int| BitvExtractRange of int * int| NonPositiveBitvType of int| ClashType of string| ClashLabel of string * string| ClashParam of string| TypeDuplicateVar of string| UnboundedVar of string| UnknownType of string| WrongArity of string * int| SymbAlreadyDefined of string| SymbUndefined of string| NotAPropVar of string| NotAPredicate of string| Unification of Ty.t * Ty.t| ShouldBeApply of string| WrongNumberofArgs of string| ShouldHaveType of Ty.t * Ty.t| ShouldHaveTypeIntorReal of Ty.t| ShouldHaveTypeInt of Ty.t| ShouldHaveTypeBitv of Ty.t| ArrayIndexShouldHaveTypeInt| ShouldHaveTypeArray| ShouldHaveTypeRecord of Ty.t| ShouldBeARecord| ShouldHaveLabel of string * string| NoLabelInType of Hstring.t * Ty.t| ShouldHaveTypeProp| NoRecordType of Hstring.t| DuplicateLabel of Hstring.t| DuplicatePattern of string| WrongLabel of Hstring.t * Ty.t| WrongNumberOfLabels| Notrigger| CannotGeneralize| SyntaxError| ThExtError of string| ThSemTriggerError| WrongDeclInTheory| ShouldBeADT of Ty.t| MatchNotExhaustive of Hstring.t list| MatchUnusedCases of Hstring.t list| NotAdtConstr of string * Ty.t| BadPopCommand of {}| ShouldBePositive of int| PolymorphicEnum of string| ShouldBeIntLiteral of stringError that can be raised by the typechecker
Errors raised when performing actions forbidden in some modes.
Errors raised while using models.
type error = | Parser_error of stringError used at parser loading
*)| Lexical_error of Loc.t * stringError used by the lexer
*)| Syntax_error of Loc.t * stringError used by the parser
*)| Typing_error of Loc.t * typing_errorError used at typing
*)| Run_error of run_errorError used during solving
*)| Warning_as_error| Dolmen_error of int * stringError code + description raised by dolmen.
*)| Mode_error of Util.mode * mode_errorError used when performing actions forbidden in some modes.
*)| Model_error of model_errorError raised while using models.
*)All types of error that can be raised
exception Error of errorval typing_error : typing_error -> Loc.t -> 'aRaise the input typing_error as Typing_error
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 -> 'aRaise 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 -> 'aRaise Mode_error (Forbidden_command str) as Error if a command is being used in a mode where it should not be available.
val report : Format.formatter -> error -> unitPrint a message on the formatter corresponding to the error