binsec.smtlib
Formula.Transformation
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
val rename_bl_var : (string -> string) -> Formula.bl_var -> Formula.bl_var
val rename_bv_var : (string -> string) -> Formula.bv_var -> Formula.bv_var
val rename_ax_var : (string -> string) -> Formula.ax_var -> Formula.ax_var
val rename_bl_term : (string -> string) -> Formula.bl_term -> Formula.bl_term
val rename_bv_term : (string -> string) -> Formula.bv_term -> Formula.bv_term
val rename_ax_term : (string -> string) -> Formula.ax_term -> Formula.ax_term
val replace_bl_term : Formula.def -> Formula.bl_term -> Formula.bl_term
val replace_bv_term : Formula.def -> Formula.bv_term -> Formula.bv_term
val replace_ax_term : Formula.def -> Formula.ax_term -> Formula.ax_term
val constant_propagation : ?keep:Formula.VarSet.t -> Formula.formula -> Formula.formula
val prune_and_inline : ?keep:Formula.VarSet.t -> Formula.formula -> Formula.formula
val read_over_write : ?lst:int -> ?rbs:bool -> ?itv:bool -> Formula.formula -> Formula.formula
val static_single_assignment : Formula.formula -> Formula.formula
val taint : (Formula.var -> bool) -> Formula.formula -> Formula.formula
val optimize : ?keep:Formula.VarSet.t -> ?lst:int -> ?cst:bool -> ?itv:bool -> ?prn:bool -> ?rbs:bool -> ?row:bool -> ?ssa:bool -> ?is_controlled:(Formula.VarSet.elt -> bool) -> Formula.formula -> Formula.formula