package binsec

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type rvalue =
  1. | Nondet
  2. | Signed_interval of Dba.Expr.t * Dba.Expr.t
  3. | Unsigned_interval of Dba.Expr.t * Dba.Expr.t
  4. | Set of Dba.Expr.t list
  5. | Singleton of Dba.Expr.t
type identifier = string
type operation =
  1. | Assignment of Dba.LValue.t * rvalue * identifier option
  2. | Mem_load of Dba.Expr.t * int
  3. | Assumption of Dba.Expr.t
  4. | Universal of Dba.LValue.t
type t = {
  1. controlled : bool;
  2. operation : operation;
}
val assume : Dba.Expr.t -> t
val assign : ?identifier:string -> ?controlled:bool -> Dba.LValue.t -> rvalue -> t
val universal : Dba.LValue.t -> t

Mark l-value as universally quantified

val from_store : ?controlled:bool -> Dba.LValue.t -> t
val from_assignment : ?identifier:string -> ?controlled:bool -> Dba.Instr.t -> t
val set_control : bool -> t -> t