binsec.smtlib
Utils.BindEnv
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
type t
type ('var, 'term) status =
| Free
| Declared of 'var * Formula.sort list
| Defined of 'var * Formula.decl list * 'term
val create : int -> t
val decl : t -> Formula.decl -> unit
val def : t -> Formula.def -> unit
val undecl : t -> Formula.decl -> unit
val undef : t -> Formula.def -> unit
val bl_lookup : t -> Formula.bl_var -> (Formula.bl_var, Formula.bl_term) status
val bv_lookup : t -> Formula.bv_var -> (Formula.bv_var, Formula.bv_term) status
val ax_lookup : t -> Formula.ax_var -> (Formula.ax_var, Formula.ax_term) status
val is_bl_cst : t -> Formula.bl_term -> bool option
val is_bv_cst : t -> Formula.bv_term -> Binsec_base.Bitvector.t option
val is_bl_var : t -> Formula.bl_term -> Formula.bl_var option
val is_bv_var : t -> Formula.bv_term -> Formula.bv_var option
val is_ax_var : t -> Formula.ax_term -> Formula.ax_var option