binsec_sse_checkct
Binsec_sse_checkct.Ct_state
binsec
binsec.base
binsec.cli
binsec.domains
binsec.dwarf
binsec.isa
binsec.kernel
binsec.script
binsec.smtlib
binsec.sse
binsec.symbolic
binsec.unix
binsec_cli_bbsse
binsec_cli_disasm
binsec_cli_ghidra
binsec_cli_sse
binsec_cli_xtrasec
binsec_isa_armv7
binsec_isa_armv8
binsec_isa_ppc64
binsec_isa_riscv
binsec_isa_sparcv8
binsec_isa_x86_32
binsec_isa_x86_64
binsec_kernel_dba
binsec_kernel_isa
binsec_kernel_loader
binsec_kernel_parser
binsec_script_ast
binsec_smtlib_bindings
binsec_sse_loader
binsec_sse_quick_merge
binsec_sse_shadow_stack
binsec_sse_stake
checkct
shadow_stack
stake
type load = ([ `Mem ], string, Binsec_sse.Symbolic.Default.Memory.t) Binsec_kernel.Term.t
type t = {
mutable constraints : Binsec_sse.Symbolic.Default.Expr.t list;
mutable conjunction : Binsec_sse.Symbolic.Default.Expr.t;
secrets : Binsec_sse.Symbolic.Default.Expr.t Binsec_sse.Symbolic.Default.Expr.Tbl.t;
mirror_e : Binsec_sse.Symbolic.Default.Expr.t Binsec_sse.Symbolic.Default.Expr.Tbl.t;
mirror_m : Binsec_sse.Symbolic.Default.Memory.t Binsec_sse.Symbolic.Default.Memory.Tbl.t;
mutable loads : load list;
roots : Binsec_sse.Symbolic.Default.Memory.t Binsec_sse.Symbolic.Default.Memory.Tbl.t;
mutable models : (int * Binsec_sse.Symbolic.Default.Model.t) list;
}
val empty : unit -> t
val fork : t -> t
val mirror : Binsec_sse.Symbolic.Default.Expr.t -> t -> unit
val is_tainted : Binsec_sse.Symbolic.Default.Expr.t -> t -> bool
val is_tainted_memory : Binsec_sse.Symbolic.Default.Memory.t -> t -> bool
val make_mirror_e : Binsec_sse.Symbolic.Default.Expr.t -> t -> Binsec_sse.Symbolic.Default.Expr.t
val make_mirror_m : Binsec_sse.Symbolic.Default.Memory.t -> t -> Binsec_sse.Symbolic.Default.Memory.t
val make_context : Binsec_sse.Symbolic.Default.Expr.t list -> t -> unit
val find_root : Binsec_sse.Symbolic.Default.Memory.Tbl.key -> t -> Binsec_sse.Symbolic.Default.Memory.t