package binsec

  1. Overview
  2. Docs
On This Page
  1. Constructors
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t = private
  1. | Assign of LValue.t * Expr.t * id
  2. | SJump of id jump_target * tag option
  3. | DJump of Expr.t * tag option
  4. | If of Expr.t * id jump_target * id
  5. | Stop of state option
  6. | Assert of Expr.t * id
  7. | Assume of Expr.t * id
  8. | NondetAssume of LValue.t list * Expr.t * id
  9. | Nondet of LValue.t * region * id
  10. | Undef of LValue.t * id
    (*

    value of lval is undefined ** e.g. AF flag for And instruction in x86 *

    *)
  11. | Malloc of LValue.t * Expr.t * id
  12. | Free of Expr.t * id
  13. | Print of printable list * id
Constructors
val assign : LValue.t -> Expr.t -> int -> t

assign lv e successor_id creates the assignment of expression e to l-value lv, going to DBA instruction successor id

val ite : Expr.t -> id Jump_target.t -> int -> t
val undefined : LValue.t -> int -> t
val non_deterministic : ?region:region -> LValue.t -> int -> t
val static_jump : ?tag:Tag.t -> id Jump_target.t -> t
val static_inner_jump : ?tag:Tag.t -> int -> t
val static_outer_jump : ?tag:Tag.t -> Virtual_address.t -> t
val call : return_address:address -> id Jump_target.t -> t
val dynamic_jump : ?tag:Tag.t -> Expr.t -> t
val malloc : LValue.t -> Expr.t -> int -> t
val free : Expr.t -> int -> t
val _assert : Expr.t -> int -> t
val assume : Expr.t -> int -> t
val non_deterministic_assume : LValue.t list -> Expr.t -> int -> t
val stop : state option -> t
val print : printable list -> int -> t