Module Dba.InstrSource

Sourcetype 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

Sourceval 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

Sourceval ite : Expr.t -> id Jump_target.t -> int -> t
Sourceval undefined : LValue.t -> int -> t
Sourceval non_deterministic : LValue.t -> int -> t
Sourceval static_jump : ?tag:Tag.t -> id Jump_target.t -> t
Sourceval static_inner_jump : ?tag:Tag.t -> int -> t
Sourceval static_outer_jump : ?tag:Tag.t -> Binsec_base.Virtual_address.t -> t
Sourceval call : return_address:address -> id Jump_target.t -> t
Sourceval dynamic_jump : ?tag:Tag.t -> Expr.t -> t
Sourceval _assert : Expr.t -> int -> t
Sourceval assume : Expr.t -> int -> t
Sourceval stop : state option -> t