package alt-ergo-lib

  1. Overview
  2. Docs
package alt-ergo-lib
Legend:
Library
Module
Module type
Parameter
Class
Class type

Errors module

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

Error types

type typing_error =
  1. | BitvExtract of int * int
  2. | BitvExtractRange of int * int
  3. | ClashType of string
  4. | ClashLabel of string * string
  5. | ClashParam of string
  6. | TypeDuplicateVar of string
  7. | UnboundedVar of string
  8. | UnknownType of string
  9. | WrongArity of string * int
  10. | SymbAlreadyDefined of string
  11. | SymbUndefined of string
  12. | NotAPropVar of string
  13. | NotAPredicate of string
  14. | Unification of Ty.t * Ty.t
  15. | ShouldBeApply of string
  16. | WrongNumberofArgs of string
  17. | ShouldHaveType of Ty.t * Ty.t
  18. | ShouldHaveTypeIntorReal of Ty.t
  19. | ShouldHaveTypeInt of Ty.t
  20. | ShouldHaveTypeBitv of Ty.t
  21. | ArrayIndexShouldHaveTypeInt
  22. | ShouldHaveTypeArray
  23. | ShouldHaveTypeRecord of Ty.t
  24. | ShouldBeARecord
  25. | ShouldHaveLabel of string * string
  26. | NoLabelInType of Hstring.t * Ty.t
  27. | ShouldHaveTypeProp
  28. | NoRecordType of Hstring.t
  29. | DuplicateLabel of Hstring.t
  30. | DuplicatePattern of string
  31. | WrongLabel of Hstring.t * Ty.t
  32. | WrongNumberOfLabels
  33. | Notrigger
  34. | CannotGeneralize
  35. | SyntaxError
  36. | ThExtError of string
  37. | ThSemTriggerError
  38. | WrongDeclInTheory
  39. | ShouldBeADT of Ty.t
  40. | MatchNotExhaustive of Hstring.t list
  41. | MatchUnusedCases of Hstring.t list
  42. | NotAdtConstr of string * Ty.t
  43. | BadPopCommand of {
    1. pushed : int;
    2. to_pop : int;
    }
  44. | ShouldBePositive of int

Error that can be raised by the typechecker

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

Errors that can be raised at solving

type error =
  1. | Parser_error of string
    (*

    Error used at parser loading

    *)
  2. | Lexical_error of Loc.t * string
    (*

    Error used by the lexer

    *)
  3. | Syntax_error of Loc.t * string
    (*

    Error used by the parser

    *)
  4. | Typing_error of Loc.t * typing_error
    (*

    Error used at typing

    *)
  5. | Run_error of run_error
    (*

    Error used during solving

    *)
  6. | Warning_as_error

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 -> Loc.t -> '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

Printing

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

Print a message on the formatter corresponding to the error