Binsec_symbolic.StateSourceRaised by reasoning functions (S.check_sat and ENUMERATION.next) when no solution has been found within the resource budget (e.g. SetSMTSolverTimeout).
Raised by the DATA.lookup function when the variable is not defined.
Raised by the DATA.read, DATA.select, S.write and S.store functions when the memory array is not defined.
Extends the booleans with Unknown.
A size in bit.
and 'a operator = 'a Binsec_kernel.Term.operator = | Not : unary operator| Sext : size -> unary operator| Uext : size -> unary operator| Restrict : int interval -> unary operator| Plus : binary operator| Minus : _ operator| Mul : binary operator| Udiv : binary operator| Urem : binary operator| Sdiv : binary operator| Srem : binary operator| Or : binary operator| And : binary operator| Xor : binary operator| Concat : binary operator| Lsl : binary operator| Lsr : binary operator| Asr : binary operator| Rol : binary operator| Ror : binary operator| Eq : binary operator| Diff : binary operator| Ule : binary operator| Ult : binary operator| Uge : binary operator| Ugt : binary operator| Sle : binary operator| Slt : binary operator| Sge : binary operator| Sgt : binary operatorA 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
type feature += | ValueKind : ('value, 'state, 'cookie, 'value value_kind) feature| SetSMTSolver : ('value,
'state,
'cookie,
'cookie ->
Binsec_symbolic.Smtlib.Solver.backend ->
unit)
feature| SetSMTSolverTimeout : ('value, 'state, 'cookie, 'cookie -> float -> unit)
feature| SetSMTDumpDir : ('value, 'state, 'cookie, 'cookie -> string -> unit) feature| SetSMTSolverMultiChecks : ('value, 'state, 'cookie, 'cookie -> bool -> unit)
feature| ToFormula : ('value,
'state,
'cookie,
'state ->
Binsec_symbolic.Smtlib.Formula.formula)
feature