package binsec

  1. Overview
  2. Docs
package binsec
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Binsec_symbolic.StateSource

Sourceexception Unknown

Raised by reasoning functions (S.check_sat and ENUMERATION.next) when no solution has been found within the resource budget (e.g. SetSMTSolverTimeout).

Sourceexception Undefined of Binsec_kernel.Dba.Var.t

Raised by the DATA.lookup function when the variable is not defined.

Sourceexception Undeclared of string option

Raised by the DATA.read, DATA.select, S.write and S.store functions when the memory array is not defined.

Sourceexception Non_mergeable

Raised by the S.merge function the two states can not be merged.

Extends the booleans with Unknown.

A size in bit.

Sourceand 'a operator = 'a Binsec_kernel.Term.operator =
  1. | Not : unary operator
  2. | Sext : size -> unary operator
  3. | Uext : size -> unary operator
  4. | Restrict : int interval -> unary operator
  5. | Plus : binary operator
  6. | Minus : _ operator
  7. | Mul : binary operator
  8. | Udiv : binary operator
  9. | Urem : binary operator
  10. | Sdiv : binary operator
  11. | Srem : binary operator
  12. | Or : binary operator
  13. | And : binary operator
  14. | Xor : binary operator
  15. | Concat : binary operator
  16. | Lsl : binary operator
  17. | Lsr : binary operator
  18. | Asr : binary operator
  19. | Rol : binary operator
  20. | Ror : binary operator
  21. | Eq : binary operator
  22. | Diff : binary operator
  23. | Ule : binary operator
  24. | Ult : binary operator
  25. | Uge : binary operator
  26. | Ugt : binary operator
  27. | Sle : binary operator
  28. | Slt : binary operator
  29. | Sge : binary operator
  30. | Sgt : binary operator
Sourcemodule type UID = sig ... end
Sourcemodule type VALUE = sig ... end
Sourcemodule type MODEL = sig ... end
Sourcemodule type ENUMERATION = sig ... end
Sourcemodule type DATA = sig ... end
Sourcetype ('value, 'state, 'cookie, 'a) feature = ..

A feature is a state functionality that is not part of the common interface.

A value of type 'a can be queried with the function S.more. It can be anything, including a function, and may depend on the type parameters 'value, 'state and 'cookie.

For instance, the function S.lookup can be expressed as a !type-feature as follows. type ('value, 'state, 'cookie, 'a) feature += | Lookup : ('value, 'state, 'cookie, Dba.Var.t -> 'state -> 'value) feature

Sourcemodule type S = sig ... end
Sourcetype _ value_kind = ..

A witness of the value type used by the state (S.more ValueKind).

Sourcetype feature +=
  1. | ValueKind : ('value, 'state, 'cookie, 'value value_kind) feature
  2. | SetSMTSolver : ('value, 'state, 'cookie, 'cookie -> Binsec_symbolic.Smtlib.Solver.backend -> unit) feature
  3. | SetSMTSolverTimeout : ('value, 'state, 'cookie, 'cookie -> float -> unit) feature
  4. | SetSMTDumpDir : ('value, 'state, 'cookie, 'cookie -> string -> unit) feature
  5. | SetSMTSolverMultiChecks : ('value, 'state, 'cookie, 'cookie -> bool -> unit) feature
  6. | ToFormula : ('value, 'state, 'cookie, 'state -> Binsec_symbolic.Smtlib.Formula.formula) feature