package alt-ergo-lib

  1. Overview
  2. Docs
The Alt-Ergo SMT prover library

Install 

dune-project
 Dependency

alt-ergo.ocamlpro.com Readme Changelog LicenseRef-OCamlpro-Non-Commercial; Apache-2.0 License Edit opam file Versions (15)

Authors

  1. A
    Alt-Ergo developers <alt-ergo@ocamlpro.com>

Maintainers

  1. A
    Alt-Ergo developers <alt-ergo@ocamlpro.com>

Sources

alt-ergo-2.6.0.tbz
sha256=1269311af25278a466892ba878cc888ba59f177f53dd03f12a2c623b03fcf37e
sha512=8a841e1f295e889fa9cb95aa4021bbb481d73279e99512c2afb3510e1f6c9d367113ee6bd3a90bc51111fa3e766a302633e9d5d18fde7660b139cd19a271eb23

doc/alt-ergo-lib/AltErgoLib/Errors/index.html

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

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. | 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
  7. | Dolmen_error of int * string
    (*

    Error code + description raised by dolmen.

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

    Error used when performing actions forbidden in some modes.

    *)
  9. | 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 -> 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

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 : Format.formatter -> error -> unit

Print a message on the formatter corresponding to the error