Module Binsec_kernel_dba.PredbaSource

First IL before producing DBA

Sourcetype '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
Sourceval assign : Dba.LValue.t -> Dba.Expr.t -> 'a t
Sourceval (<<-) : Dba.LValue.t -> Dba.Expr.t -> 'a t
Sourceval static_jump : ?tag:Dba.tag -> 'a Dba.jump_target -> 'a t
Sourceval dynamic_jump : ?tag:Dba.tag -> Dba.Expr.t -> 'a t
Sourceval dynamic_assert : Dba.Expr.t -> 'a t
Sourceval conditional_jump : Dba.Expr.t -> 'a Dba.jump_target -> 'a t
Sourceval undefined : Dba.LValue.t -> 'a t
Sourceval non_deterministic : Dba.LValue.t -> 'a t
Sourceval stop : Dba.state -> 'a t
Sourceval blockify : Dba.address -> Dba.id t list -> Dhunk.t

blockify next_addr predbas

  • returns

    a full DBA block considering it continues to next_addr