package binsec

You can search for identifiers within the package.

in-package search v0.2.0

Semantic analysis of binary executables

Install

sha256=2f990f80ebd06b71af4fde46c6a248eb74d52c6f46be63bdf97d99f72589db13

sha512=38d93ae20ae58e10027eb0f7669d3ab960ddc640526018fc94008ccd6cb63ec99030d0ee39dfb9cbd0d5e144db4615c9027bd2adcb197fc75676c45dbb54f836

type t = private

| Assign of LValue.t * Expr.t * id
| SJump of id jump_target * tag
| DJump of Expr.t * tag
| If of Expr.t * id jump_target * id
| Stop of state option
| Assert of Expr.t * id
| Assume of Expr.t * id
| Nondet of LValue.t * id
| Undef of LValue.t * id
(*
value of lval is undefined ** e.g. AF flag for And instruction in x86 *
*)

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

On This Page