Module Dba.Instr

type t = private
  1. | Assign of LValue.t * Expr.t * id
  2. | SJump of id jump_target * tag
  3. | DJump of Expr.t * tag
  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. | Nondet of LValue.t * id
  9. | Undef of LValue.t * id
    (*

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

    *)
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 : 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 _assert : Expr.t -> int -> t
val assume : Expr.t -> int -> t
val stop : state option -> t