Module Binsec.Predba

First IL before producing DBA

type 'a t = private
  1. | Assign of Dba.LValue.t * Dba.Expr.t
  2. | SJump of 'a Dba.jump_target * Dba.tag option
  3. | DJump of Dba.Expr.t * Dba.tag option
  4. | Assert of Dba.Expr.t
  5. | If of Dba.Expr.t * 'a Dba.jump_target
  6. | Undef of Dba.LValue.t
  7. | Nondet of Dba.LValue.t
  8. | Stop of Dba.state
val assign : Dba.LValue.t -> Dba.Expr.t -> 'a t
val (<<-) : Dba.LValue.t -> Dba.Expr.t -> 'a t
val static_jump : ?tag:Dba.tag -> 'a Dba.jump_target -> 'a t
val dynamic_jump : ?tag:Dba.tag -> Dba.Expr.t -> 'a t
val dynamic_assert : Dba.Expr.t -> 'a t
val conditional_jump : Dba.Expr.t -> 'a Dba.jump_target -> 'a t
val undefined : Dba.LValue.t -> 'a t
val non_deterministic : Dba.LValue.t -> 'a t
val stop : Dba.state -> 'a t
val blockify : Dba.address -> Dba.id t list -> Dhunk.t

blockify next_addr predbas

  • returns

    a full DBA block considering it continues to next_addr