binsec.smtlib
Solver.Make
binsec
binsec.base
binsec.cli
binsec.domains
binsec.dwarf
binsec.isa
binsec.kernel
binsec.script
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_checkct
binsec_sse_loader
binsec_sse_quick_merge
binsec_sse_shadow_stack
binsec_sse_stake
checkct
shadow_stack
stake
module S : sig ... end
type t
val pp : Format.formatter -> t -> unit
val create : theory:string -> S.arg -> t
val destroy : t -> unit
val run : t -> 'a command -> 'a
val put_entry : t -> Formula.entry -> unit
val check_sat : timeout:float -> t -> Formula.status
val get_model : t -> Binsec_smtlib__.Formula_model.t
val get_bv_value : t -> Formula.bv_term list -> Binsec_base.Bitvector.t list
val get_ax_value : t -> Formula.ax_term -> (Binsec_base.Bitvector.t * Binsec_base.Bitvector.t) array