Index of values

(&&) [Transfer_functions.Boolean_Backward]
(||) [Transfer_functions.Boolean_Backward]

abs_big_int [Bigint]
abvexpr_equal [Smtlib2]
add [Worklist.S]
add [Sigs.Arithmetic]
add [Parse_helpers.Declarations]
add [Dba_types.Expr]
add [Basic_types.Size]
add [Basic_types.Natural]
add_alias [Call_convention.CallConvention]
add_big_int [Bigint]
add_bytes [Binpatcher.PatchMap]
add_bytes address bytes patchmap writes the opcode bytes to address in the patchmap.
add_chained_instr [Disasm_types]
add_comment [Formula]
Add a comment in in the formula (considered as a command)
add_constraint [Formula]
add the given smt_expr as constraint in the formula
add_id [Dba_types.Caddress]
add_initial_state [Formula]
Initialize the memory with all the values given in the map
add_int [Dba_types.Virtual_address]
add_int [Dba_types.Caddress]
add_int addr n Increment the current address from the value of n
add_int [Basic_types.Natural]
add_int_big_int [Bigint]
add_smt_cond [Concrete_eval]
add_symbolic_input [Formula]
add_symbolic_input name size add a new bitvector in the formula.
add_virtual_addresses [Disasm_core.W]
advance [Lreader]
advance r n moves the cursor the cursor n bytes.
alizarin [Colors.FlatUI]
amethyst [Colors.FlatUI]
analyse [Ai.AbstractAnalysis]
and_big_int [Bigint]
append [Region_bitvector]
append [Dba_types.Expr]
append [Bitvector.Common]
append_int [Basic_types.Binstream]
append_int64 [Basic_types.Binstream]
apply_default_stub [Libcall_stubs]
apply_libcall_policy [Libcall_stubs]
apply_policy [Libcall_types.LibCall]
apply_smt_elements_recovery [Normalize_instructions]
apply_smt_natural_cond_recovery [Normalize_predicate]
arg [Simulate_options.SemanticsMode]
arg [Parameters.Generic]
arg_dse [Options]
arith_op_to_string [X86Util]
asbestos [Colors.FlatUI]
assert_failure [Errors]
assign [Predba]
assign [Dba_types.Instruction]
assign_to_f [Normalize_instructions]
assume [Dba_types.Instruction]

backend_port [Options]
Internal port server<->workers
backward_refine_elements [Backward_analysis]
bad [Disasm_types.Mnemonic]
band [Transfer_functions.Binary_Backward]
base_value [Dba_types.Caddress]
bashr [Transfer_functions.Binary_Backward]
basic [Simulate_options.SemanticsMode]
basic_affine [Simulate_options.SemanticsMode]
bconcat [Transfer_functions.Binary_Backward]
belizehole [Colors.FlatUI]
beq [Transfer_functions.Binary_Backward]
bextract [Transfer_functions.Binary_Backward]
biadd [Transfer_functions.Binary_Backward]
biconst [Transfer_functions.Binary_Forward]
big_int_of_int [Bigint]
big_int_of_int32 [Bigint]
big_int_of_int64 [Bigint]
big_int_of_nativeint [Bigint]
big_int_of_string [Bigint]
bimul [Transfer_functions.Binary_Backward]
bin_of_bool [Generic_decoder_sig.Expr_Input]
bin_to_explore [Options]
binary [Dba_types.Expr]
binary boperator loperand roperand creates a binary expression from boperator with left operand loperand and right operand roperand.
binary [Dba_to_smtlib]
convert a DBA binary operator to a Smtlib binary operator
binary_ops [Dba_printer.Renderer]
bind [Generic_decoder_sig.Monad]
bisdiv [Transfer_functions.Binary_Backward]
bisle [Transfer_functions.Binary_Backward]
bislt [Transfer_functions.Binary_Backward]
bismod [Transfer_functions.Binary_Backward]
bisub [Transfer_functions.Binary_Backward]
bits1 [Basic_types.BitSize]
bits128 [Basic_types.BitSize]
bits16 [Basic_types.BitSize]
bits32 [Basic_types.BitSize]
bits64 [Basic_types.BitSize]
bits8 [Basic_types.BitSize]
bitsize [Dba_types.LValue]
bitsize_of_mode [X86Util]
bitsize_of_simd_size [X86Util]
bitsize_of_szmode [X86Util]
bitsize_of_xmm_mm [X86Util]
bitvector_of [Region_bitvector]
biudiv [Transfer_functions.Binary_Backward]
biule [Transfer_functions.Binary_Backward]
biult [Transfer_functions.Binary_Backward]
biumod [Transfer_functions.Binary_Backward]
block_simplifications [Simplification_dba_block]
block_start [Dba_types.Caddress]
block_start bv i create bv 0
block_start_of_int [Dba_types.Caddress]
blockify [Predba]
blockify next_addr predbas
blshr [Transfer_functions.Binary_Backward]
bool_any [Interval.S]
bool_false [Interval.S]
bool_false [Dba_types.Expr]
bool_of_bin [Generic_decoder_sig.Expr_Input]
bool_true [Interval.S]
bool_true [Dba_types.Expr]
Encoding of booleans as DBA expressions
bor [Transfer_functions.Binary_Backward]
bottom [Union_find.Make]
bottom [High_level_predicate]
bsext [Transfer_functions.Binary_Backward]
bshl [Transfer_functions.Binary_Backward]
buext [Transfer_functions.Binary_Backward]
build_analysis_configuration [Conf_exploration]
build_formula_file [Formula]
same as build_formula_file but provide a file name in which to output the generated formula
build_formula_incremental [Formula]
build_formula_incremental pred ~ksteps ~forward ~pruning ~push ~file session solver pred predicate to check (if none just provide SmtTrue), ~ksteps indicate the number of backward steps to perform when running backward, ~forward indicate weither or not the formula should be built forward or not (default forward), ~pruning don't modify this parameter, ~push indicate weither or not to push before adding the predicate, ~file debug file to write output into, session solver session in which to send to request, solver solver used to solve
bvexpr_equal [Smtlib2]
bvone [Smtlib2]
smt_bv_expr which value is 1 of size 1
bvzero [Smtlib2]
bxor [Transfer_functions.Binary_Backward]
bytesize [Basic_types.Constants]
bytesize_of_mode [X86Util]
bytesize_of_simd_size [X86Util]
bytesize_of_szmode [X86Util]
bytesize_of_xmm_mm [X86Util]

call [Dba_types.Instruction]
callees [Dba_types.Block]
callees b computes the set of addresses this block may call
cand [Dba_types.Condition]
carrot [Colors.FlatUI]
cc_to_string [X86Util]
cfg_file [Options]
Output CFG file
cfgraph [Options]
Option set to print cfgraph
change_variable [Formula]
main function to change a variable value in the formula.
channel_get_color [Logger.S]
channel_set_color [Logger.S]
set_channel_color b chan activates (if b is true) or deactivates (if b is false) the emission of ANSI color tags for terminal.
check_consistency [Libcall_types.LibCall]
check_consistency_memory_t [Libcall_utils]
check_free [Domain_common]
check_init [Options]
check_libcall_policy_consistency [Libcall_stubs]
check_options [Options]
Check that a file has been set when a mode type needs it
checked_cond_expr [Parse_helpers.Mk]
checked_localized_instruction [Parse_helpers.Mk]
checksize_address [Dba_utils]
checksize_dbacond [Dba_utils]
checksize_instruction [Dba_utils]
clear_bit [Bitvector.Common]
cli [Binpatcher_options]
cli_handler [Simulate_options.ConditionalStrategy]
cli_handler [Logger.S]
cli_handler [Disasm_options.DisassemblyMode]
cli_handler [Ai_options.Domain]
clouds [Colors.FlatUI]
cnot [Dba_types.Condition]
Construction functions
command [Options]
Hold the command select
compare [Sigs.Comparable]
compare [Region_bitvector.SubSymb]
compare_big_int [Bigint]
complete_all_partial_trace [Trace_loader]
read all chunks in the channel and put them in the trace
complete_partial_trace [Trace_loader]
complete_partial_trace trace chunk keep complete trace with the chunk chunk.
computesize_dbaexpr [Dba_utils]
computesize_dbalhs [Dba_utils]
conc_infos_available [Trace_type]
are concrete infos available
concat [Bitvector.Common]
concrete [Colors.FlatUI]
concretize_memory [Formula_utils]
concretize_memory dba_addr data env add constraints on the memory at the logical address dba_addr for every bytes of data
concretize_register [Formula_utils]
concretize_register name value env concretize the register name with the value value.
cond [Generic_decoder.Decode_Expr]
cond_to_f [Normalize_instructions]
condition_to_string [X86Util]
config [Options]
Hold the current DSE configuration
config_seed_file [Options]
cons [Worklist.CMake]
cons e h inserts e at the front of the worklist h
constant [Smtlib2]
constant [Parse_helpers.Mk.Expr]
constant [Dba_types.Expr]
constant ~region bv creates a constant expression from the bitvector bv from region region.
contains [Interval.S]
contains_lhs [Dba_utils]
contains_variable [Formula]
contains_zero [Interval.S]
control_reg_to_string [X86Util]
copy [File_utils]
copy src dst copies filename src to filename dst
copy [Dba_types.Block]
copy_equalities [Union_find.Make]
cor [Dba_types.Condition]
counter_conf [Conf_exploration]
create [Disasm_types.Instruction]
create [Disasm_types.BasicInstruction]
create [Binpatcher.WritableLoader]
create [Union_find.Make]
create [Interval.S]
create [Disasm.Program]
create [Dba_types.Statement]
create [Dba_types.Virtual_address]
create [Dba_types.Caddress]
create [Bitvector.Common]
create [Basic_types.Size]
create [Basic_types.Natural]
create_constant [Region_bitvector]
create_constant v sz creates a bitvector of value bv with size sz in region `Constant
create_from_files [Binpatcher.WritableLoader]
create_from_files ~executable ~patch_file creates a writable loader from a binary file and a series of patches read from a given file
create_from_tuple [Bitvector.Common]
create_qed_checker [Qed]
Returns a Qed.qed_checker form a formula.
creified [Dba_types.Condition]
cur_address [Parse_helpers]

debug [Logger.S]
debug ~level:n msg will be displayed if at least level n + 1 debug is activated
debug_channel [Logger.S]
These predefined channels are flushed after each call and a newline character is inserted.
debug_file [Options]
Output debug file
debug_reg_to_string [X86Util]
declared [Parse_helpers.Mk.Lhs]
declared_id [Parse_helpers.Mk.Expr]
declared_restricted [Parse_helpers.Mk.Lhs]
decode [X86toDba]
decode [Disasm_core]
decode addr decodes the contents of address addr
decode [ArmToDba]
decode [Options]
Option set to only disassemble an opcode
decode [Disasm]
decode s decodes the string opcode s.
decode_bin_opcode [Decode_utils]
decode_hex_opcode [Decode_utils]
decode_llvm [Options]
Option set to only disassemble an opcode to LLVM
decode_llvm [Disasm]
decode s decodes the string opcode s.
decode_opcode [Decode_utils]
decode_string [X86toDba]
default [Infos]
Constructors and modificators
default_get_byte_region_at [Region_bitvector]
default_get_byte_region_at addr is get_byte_region_at addr but catches the possible exception and returns an undefined byte instead.
default_global_widening_delay [Infos]
default_global_widening_thresholds [Infos]
default_init [Dba_types.Caddress]
default_session [Solver]
default session constructor
default_stub [Call_convention.CallConvention]
diff [Sigs.Comparisons]
diff [Region_bitvector]
diff [Interval.S]
diff [Dba_types.Expr]
dim [Binpatcher.WritableLoader]
dim t gives the size of the loaded image in bytes
disassemble [Disasm.Recursive]
disassemble [Disasm]
dispatch_instruction [Instruction_stubs]
Dispatch an instruction ident to the right symbolic stub
dispatch_syscall [Syscall_stubs]
Dispatch the current syscall infos to the right stub.
display [Concrete_state]
display_results [Simplification_dba_utils]
display_statistics [Region_bitvector]
display_statistics [Options]
div [Basic_types.Size]
div_big_int [Bigint]
doc [Parameters.Builder.ParameterDeclaration]
drop [List_utils]
drop n l removes the n first elements of list l if n is greater than the length of the list, returns [].
dse_trace [Options]
dse_type [Options]
dynamic_jump [Predba]
dynamic_jump [Dba_types.Instruction]

emerland [Colors.FlatUI]
empty [Worklist.S]
empty [Disasm_types.Instruction]
empty [Binpatcher.PatchMap]
The empty patch map
empty [Smt_model]
empty [High_level_predicate]
empty [Disasm.Program]
empty [Dba_types.Block]
empty [Basic_types.Binstream]
empty_formula [Formula_type]
create an empty formula
empty_inst [Trace_type]
empty_trace [Trace_type]
end_analysis [Dse.DSE]
endiannesses [Dba_printer.Renderer]
eq [Region_bitvector]
eq [Interval.S]
eq [Dba_types.Expr]
eq [Basic_types.Natural]
eq_big_int [Bigint]
equal [Sigs.Comparisons]
equal [Sigs.Eq]
equal [Region_bitvector]
equal [Interval.S]
equal [Dba_types.Caddress]
equal [Basic_types.Size]
error [Logger.S]
For error messages only.
error_channel [Logger.S]
eval [Simplification_dba_block.Constant_propagation]
eval_alternatives [Dba_utils]
eval_cond [Concrete_eval]
eval_expr [Concrete_eval]
eval_expr_policy [Policy_engine]
exists [String_utils]
experiment [Options]
Experimental purposes only
exploration_timeout [Options]
explore [Dse.DSE]
expr [Generic_decoder.Decode_Expr]
expr_equal [Smtlib2]
expr_of_name [Parse_helpers]
expr_size [Parse_helpers]
extend [Interval.S]
extend [Bitvector.Common]
extend_signed [Interval.S]
extend_signed [Bitvector.Common]
extend_unsafe [Bitvector.Common]
extension [Region_bitvector]
extract [Smt_model]
extract model extracts relevant information in SMT-LIB model concerning ** registers and memory values.
extract [Bitvector.Common]
extract_big_int [Bigint]

false_ [Transfer_functions.Boolean_Forward]
fatal [Logger.S]
For messages that show a fatal failure, In this case, you should not be able to continue and exit code should follow the emission.
fatal_channel [Logger.S]
fflags [Options]
filemode [Parse_helpers.Mk]
fill [Bitvector.Common]
fill lo hi n returns a bitvector of size n where bits from lo to hi are set to one.
filter [String_utils]
filter p s creates a copy of s containing the characters of s such that p c = true,
finalsize [Options]
find [Union_find.Make]
find_address_content [Smt_model]
Not yet implemented
find_address_contents [Smt_model]
find_address_contents model addr find the (byte-sized) value of address ** addr from the model.
find_exec_right [Dba_types.Rights]
find_file [Options.ShareDirectory]
find_read_right [Dba_types.Rights]
find_register [Smt_model]
find_register model name finds the bitvector value of register name in ** the model ** Raise Not_found
find_section [Loader_utils]
find_write_right [Dba_types.Rights]
flag [Dba_types.LValue]
flag ~size ~subflag fname creates a variable whose flag is of the subtype subflag.
flag [Dba_types.Expr]
flag ~bits flagname constructs a variable named flagname tagged as a flag.
flag_to_offset [X86Util]
flag_to_string [X86Util]
flat [Simulate_options.SemanticsMode]
flat_map [List_utils]
flat_map f l is like f l |> List.flatten but tail-recusrive and more efficient
flat_or_basic_and_full [Simulate_options.SemanticsMode]
flat_or_not_basic [Simulate_options.SemanticsMode]
flatten_memory [Options]
Remove the array theory from formula generated.
flatten_to_arrays_tuple [Infos.WideningThreshold]
flip_bit [Bitvector.Common]
float_of_big_int [Bigint]
float_reg_to_string [X86Util]
fold [Worklist.S]
fold [Disasm_core.Make]
fold [Disasm_core]
fold f wl v starts disassembly from worklist wl (i.e.
fold [String_utils]
fold f acc s computes (f ....
fold_expr [Dba_utils.Expr]
fold_left [Dba_types.Block]
for_all [String_utils]
for_all [Dba_types.Block]
free [Dba_types.Instruction]
ftemps [Options]

gcd_big_int [Bigint]
ge [Basic_types.Natural]
ge_big_int [Bigint]
gen_undef [Smt_bitvectors]
generate_dbalist [Dba_io]
convert a list of dbainstr to a list DBA in the Piqi format
geqS [Region_bitvector]
geqU [Region_bitvector]
get [Machine.Gettable_settable]
get [Binpatcher.WritableLoader]
get addr t gets the byte stored at address addr
get [Simulate_options.ConditionalStrategy]
get [Options.ExecFile]
get [Disasm_options.DisassemblyMode]
Defaults to Recursive
get [Dba_types.Block]
get [Parameters.Generic]
get [Ai_options.Domain]
get_alive_branches [Disasm_dyn_infos]
get_bit [Bitvector.Common]
get_byte [Basic_types.Binstream]
get_byte b n retrieves byte number n from b
get_byte_at [Loader_utils]
get_byte_region_at [Region_bitvector]
get_byte_region_at addr returns the value read at the lone byte cell addr.
get_caddress [Disasm_types.Instruction]
Other accessors
get_color [Logger.S]
get_conf_id [Conf_exploration]
get_conf_name [Conf_exploration]
get_dba_configuration_filename [Options]
get_dba_filename [Options]
get_debug_level [Logger.S]
get_describe_binary [Options]
get_elements [Union_find.Make]
get_endianness [Dba_types]
get_entry_point [Options]
get_expr [Region_bitvector]
get_file [Disasm_options]
get_flag_value [X86Util]
get_img [Loader_utils]
get_info_level [Logger.S]
get_libcall [Trace_type]
return the concrete informations of the library call
get_load_addr [Trace_type]
get the load address of the value read by the instruction
get_load_content [Trace_type]
get the load content read by the instruction
get_load_content [Trace_loader]
get_load_content addr ~esp_value size infos return the runtime data read in memory at addr of size size in the instruction concrete informations info
get_lower_bound [Normalize_instructions]
get_merge_stats [Trace_postprocessing]
get_nb_classes [Union_find.Make]
get_nb_names [Union_find.Make]
get_nb_undef_builds [Simulate_utils]
get_next_address [Trace_type]
next address for the current instruction
get_next_address_bv [Trace_type]
return the next address as a Bitvector given an address size
get_opt_or_default [Utils]
Option types
get_param [Call_convention.CallConvention]
get_reg_value [Trace_type]
return the given register value as read or written using the switch ?read (default is read)
get_reg_write_or_read_value [Trace_type]
return the given written register.
get_regread_value_bv [Trace_type]
same as get_reg_value ~read:true but return a Bitvector.t
get_regwrite_value_bv [Trace_type]
same as get_reg_value ~read:false but return a Bitvector.t
get_row_stats [Formula_optim]
get_slice [Lreader]
get_store_addr [Trace_type]
get the address of the value stored by the instruction
get_store_content [Trace_type]
get the content of the value stored by the instruction
get_syscall [Trace_type]
return the syscall infos of the instruction (use it with is_syscall)
get_syscall_name [Trace_type]
return the syscall name in case the isntruction is a syscall
get_undef_loads [Simulate_utils]
get_upper_bound [Normalize_instructions]
get_value [Region_bitvector]
get_var [Generic_decoder_sig.Expr_Input]
get_var_dbainstr [Dba_visitor]
get_var_or_create [Formula]
get a variable logical expression or create it if not existing.
get_varindex [Formula]
get_virtual_cursor [Lreader]
get_warning_level [Logger.S]
globalize_address [Dba_utils]
globalize_address root addr generates a global address from addr, * rooting it at root if it is local.
greensea [Colors.FlatUI]
gt [Basic_types.Natural]
gtS [Region_bitvector]
gtU [Region_bitvector]
gt_big_int [Bigint]

handled [Disasm_types.Mnemonic]
handled_instructions [X86toDba]
insertions / unique insertions
has_entry_points [Infos]
has_inbound_inner_jumps [Dba_types.Block.Check]
has_inverse [Dba_types.BinaryOperator]
hd_hd [List_utils]
hd_hd l gets the two first elements of a list.
hex_string_to_bin [Decode_utils]
high [Interval.S]

iassert [Dba_types.Instruction]
iflags [Options]
incr_address [Parse_helpers]
incr_undef_loads [Simulate_utils]
info [Logger.S]
Any info that should be displayed
info_channel [Logger.S]
init [Dba_types.Block]
initsize [Options]
inner [Dba_types.Jump_target]
instruction [Generic_decoder.Decode_Instr]
instruction [Dba_types.Statement]
instruction_of_string [Parse_utils]
int32_of_big_int [Bigint]
int64_of_big_int [Bigint]
int64_to_char [Decode_utils]
int64_to_littleendian_bin [Decode_utils]
int_of_big_int [Bigint]
int_to_arith_op [X86Util]
int_to_cc [X86Util]
int_to_condition [X86Util]
int_to_control_reg [X86Util]
int_to_debug_reg [X86Util]
int_to_float_reg [X86Util]
int_to_mmx_reg [X86Util]
int_to_reg32 [X86Util]
int_to_rotate_op [X86Util]
int_to_scale [X86Util]
int_to_segment_reg [X86Util]
int_to_shift_op [X86Util]
int_to_sse [X86Util]
int_to_test_reg [X86Util]
int_to_xmm_reg [X86Util]
invalid_address [Errors]
invert [Dba_types.BinaryOperator]
invert t inverts t if it has an inverse version.
ip_address [Options]
IP address to listen on
is_boolector [Solver]
check that the given solver is boolector
is_call [Dba_types.Instruction]
is_call t returns true if the instruction is a function call.
is_concrete_infos_retrieved [Trace_type]
is_decoded [Disasm_types.Instruction]
is_disjoint [Interval.S]
is_empty [Worklist.S]
is_empty [List_utils]
is_empty l returns true if l = []
is_empty [Dba_types.Block]
is_equal_smtBvExpr [Smt_bitvectors]
is_expr_translatable [Dba_types.LValue]
is_expr_translatable e returns true is the expression can have a valid lvalue translation
is_flag [Dba_types.LValue]
is_ignored_segment [Disasm_options]
is_int_big_int [Bigint]
is_libcall [Trace_type]
return either or not the instruction is call to an external library
is_max [Dba_types.Expr]
is_max e is true if e is a constant representing the maximum value for ** its size
is_max_sbv [Bitvector.Common]
is_max_ubv t (resp.
is_max_ubv [Bitvector.Common]
is_mem_call [Disasm_dyn_infos_callrets]
is_memory_set [Smt_model]
is_memory_set model address checks if the given address is present in the ** memory of this model
is_neg [Bitvector.Common]
is_none [Utils]
is_none vopt tests if vopt is indeed None.
is_not_mayused [Simplification_dba_utils]
is_one [Dba_types.Expr]
is_one e is true if e's value is equal to 1 whatever its length is
is_one [Bitvector.Common]
is_zero t (resp.
is_ones [Bitvector.Common]
is_zeros t (resp.
is_point [Interval.S]
is_same_class [Union_find.Make]
is_sat [Normalize_instructions]
is_set [Options.ExecFile]
is_set [Parameters.OptionalGeneric]
is_symbolic [Dba_types.Expr]
is_symbolic [Dba_types.Condition]
is_syscall [Trace_type]
return either or not the instruction is a syscall
is_syscall_opcode [Syscall_stubs]
return whether the given opecode is a syscall or not.
is_temporary [Dba_types.LValue]
is_traced [Trace_type]
return true if the instruction is a libcall and the call is traced
is_unit [Interval.S]
is_unknown [Machine]
is_zero [Region_bitvector]
is_zero [Dba_types.Expr]
is_zero e is true if e's value is equal to 0 whatever its length is
is_zero [Bitvector.Common]
is_zero [Basic_types.Size]
is_zeros [Bitvector.Common]
ite [Dba_types.Instruction]
ite [Dba_types.Expr]
ite cond then_e else_e creates Dba.ExprIte(cond, then_e, else_e)
itemps [Options]
iter [Worklist.S]
iter [Disasm_core.Make]
iter [Disasm_core]
iter f worklist iterates disassembles an executable with function f.
iter [Dba_types.Block]
iteri [Dba_types.Block]

jif [Predba]
join [Union_find.Make]
join [Interval.S]
join [High_level_predicate]

keys [Sigs.Collection.Map]

l_event [Options]
last [List_utils]
last l returns the last element of list l.
lchop [String_utils]
lchop n s removes the first n characters of string s.
le_big_int [Bigint]
left [String_utils]
left n s returns the n leftmost characters of s.
left_right_parentheses [Dba_printer.Renderer]
length [Dba_types.Block]
length [Basic_types.Binstream]
leq [High_level_predicate]
leqS [Region_bitvector]
leqU [Region_bitvector]
lhs_mayused_in_bcond [Simplification_dba_utils]
lhs_mayused_in_expr [Simplification_dba_utils]
lhs_mayused_in_lhs [Simplification_dba_utils]
lhs_mustkilled_by_lhs [Simplification_dba_utils]
libcall_to_string [Libcall_stubs]
linear [Disasm_core.Successors]
linear_bytewise [Disasm_core.Successors]
little_string_to_big_string [Decode_utils]
load [Generic_decoder_sig.Expr_Input]
load [Parse_helpers.Mk.Expr]
load [File_utils]
load filename return a string with the complete text of the file
load [Dba_types.Expr]
load_dba_definition [Binsec_utils]
load_file [Binpatcher.PatchMap]
load_file filename loads patches contained in filename
load_partial_trace_from_file [Trace_loader]
start reading a trace from the given channel.
load_partial_trace_from_string [Trace_loader]
load_partial_trace_from_string header fst_chunk create a trace from the raw header header and a first chunk chunk
load_to_smt [Normalize_instructions]
location [Dba_types.Statement]
logand [Smtlib2]
logand [Sigs.Logical]
logand [Region_bitvector]
logand [Interval.S]
logicalize_memory [Formula_utils]
logicalize_memory addr content put content at addr by performing a logical store in memory
logicalize_register [Formula_utils]
convert the DBA expression in SMT and then call replace_register
lognot [Smtlib2]
lognot [Sigs.Logical]
lognot [Region_bitvector]
lognot [Interval.S]
logor [Smtlib2]
logor [Sigs.Logical]
logor [Region_bitvector]
logor [Interval.S]
logxor [Sigs.Bitwise]
logxor [Region_bitvector]
logxor [Interval.S]
low [Interval.S]
lshift [Region_bitvector]
ltS [Region_bitvector]
ltU [Region_bitvector]
lt_big_int [Bigint]

m_init [Concrete_state]
make [Union_find.Make]
malloc [Parse_helpers.Mk.Region]
malloc [Dba_types.Instruction]
malloc [Dba_types.Region]
malloc_id [Dba_types]
mallocs [Simulate]
map [Worklist.S]
map [Interval.Unsigned]
map [Dba_types.Block]
mapi [Dba_types.Block]
mark_ignored_segments [Disasm_options]
max [Basic_types.Int64]
max_big_int [Bigint]
max_sbv [Bitvector.Common]
max_ubv n (resp.
max_ubv [Bitvector.Common]
maxify [Interval.S]
meet [Interval.S]
memory_addresses [Smt_model]
get_register model gets the list of addresses with specific values of this ** model
merge [Worklist.S]
merge_natural_conditions [Trace_postprocessing]
apply the post processing computation replacing low-level condition by higher-level conditions
midnightblue [Colors.FlatUI]
min_big_int [Bigint]
minify [Interval.S]
minus_big_int [Bigint]
mismatched_address_size [Errors]
mismatched_instruction_size [Errors]
mk [Infos.WideningThreshold]
mk_address [X86Util]
Default values are: address_mode: A32, address_base: None, address_index: None
mk_from_list [Infos.BoundThreshold]
mk_patches [Parse_helpers]
mk_sup [Simulate_utils]
mk_undef_value [Simulate_utils]
mm_reg_to_string [X86Util]
mmx_reg_to_string [X86Util]
mod_big_int [Bigint]
mul [Basic_types.Size]
mult_big_int [Bigint]
mult_int_big_int [Bigint]
must_lhs_expr_equal [Simplification_dba_utils]

name [Parameters.Builder.ParameterDeclaration]
name [Logger.ChannelGroup]
name_of [Dba_types.LValue]
name_of lval returns Some name if the lvalue is named, None otherwise
native_instructions_decoded [X86toDba]
Number of decoded instructions.
nativeint_of_big_int [Bigint]
natural_cond_enabled [Options]
Enable lifting low-level condition predicates to higher level predicates on conditional jumps
nb_conditional_cache_uses [Options]
nb_equalities_classes [Options]
nb_equalities_names [Options]
nb_equalities_refinement [Options]
nb_failed_nat_predicate_recoveries [Options]
nb_nat_predicate_recovery_tries [Options]
nb_recovered_nat_predicates [Options]
nb_refined_lhs [Options]
nb_workers [Options]
Number of parallel workers
neg [Sigs.Arithmetic]
neg [Interval.S]
nephritis [Colors.FlatUI]
new_env [Path_pred_env]
Create a new environment new_env analysis conf addr_size.
new_tmpvar [Formula]
create unique temporary variable in the formula
new_variable_name [Formula]
get a new variable name for a given variable (eg.
no_temporary_leak [Dba_types.Block.Check]
no_temporary_leak b checks the invariant that a block must always (re)define a temporary before using it.
no_undeclared_variables [Dba_types.Block.Check]
non_deterministic [Predba]
non_deterministic [Region_bitvector]
non_deterministic [Dba_types.Instruction]
non_deterministic_assume [Dba_types.Instruction]
not [Transfer_functions.Boolean_Backward]
not_yet_implemented [Errors]
nth_alloc [Options]
nth_free [Options]
nth_to_invert [Options]
nth_use [Options]
num_digits_big_int [Bigint]

of_bigint [Dba_types.Virtual_address]
of_binstream [Lreader]
of_bitsize [Basic_types.ByteSize]
of_bitvector [Dba_types.Virtual_address]
of_bool [Bitvector]
of_bool [Basic_types.Ternary]
of_bytes [Lreader]
of_bytes [Basic_types.Binstream]
of_bytes s converts a byte stream s.
of_code_address [Dba_types.Virtual_address]
of_dba_block [Disasm_types.Instruction]
of_expr [Dba_types.LValue]
of_expr e translates an expression to its lvalue equivalent if possible.
of_generic_instruction [Disasm_types.Instruction]
of_hexstring [Bitvector]
of_img [Lreader]
of_int32 [Bitvector]
of_int32 n creates a bitvector of size 32 and value n
of_int64 [Dba_types.Virtual_address]
of_int64 [Bitvector]
of_int64 n creates a bitvector of size 64 and value n
of_list [Disasm_core.W]
of_list [Binpatcher.PatchMap]
of_list l converts an association list l of addresses to opcodes to a patch map
of_list [Parse_helpers.Mk.Permissions]
of_list [Parse_helpers.Mk.Predicates]
of_list [Dba_types.Block]
of_list l assumes the list is sorted in increasing order inside the block
of_list [Dba_types.Declarations]
of_list [Basic_types.Binstream]
of_list l converts a list of integers.
of_lvalue [Dba_types.Expr]
of_nibbles [Lreader]
of_nibbles [Basic_types.Binstream]
of_nibbles s converts a string s of hexadecimal characters.
of_point [Interval.S]
one [Smtlib2]
smt_bv_expr which value is 0 of size 1
one [Dba_types.Expr]
one [Bitvector.Common]
ones [Dba_types.Expr]
ones n creates a constant expression of value 1 with length n.
ones [Bitvector.Common]
opaque_predicates_file [Options]
Opaque predicate information file (for assisted disassembly)
opcode_to_mnemonic [Instruction_stubs]
convert the binary string of the opcode to a variant of type Instruction_piqi.instr_ident
optim_str [Formula]
getting a string code representing the optimizations activated in the formula
or_big_int [Bigint]
orange [Colors.FlatUI]
outer [Dba_types.Jump_target]
outer_jumps [Dba_types.Block]
outer_jumps b computes the set of jumps to external addresses in block b.
outer_jumps [Dba_types.Instruction]
outer_jumps t returns the set of virtual addresses this instruction may jump to.
outer_jumps [Dba_types.Jump_target]

parse_chunk [Trace_loader]
Read a trace chunk in the given channel.
parse_command_line [Options]
Parse the command line
parse_dbalist [Dba_io]
convert a list of Piqi DBA instr to DBA instructions
parse_policy_from_file [Policy_engine]
parse_policy_from_string_list [Policy_engine]
patch_expr_size [Parse_helpers]
peek [Worklist.S]
perm [Concrete_eval]
permis [Concrete_eval]
peterriver [Colors.FlatUI]
pol_name [Options]
policy filename when provided on the command line
pomegranate [Colors.FlatUI]
pop [Worklist.S]
pop [Solver]
send the pop command to the solver
pop [Sigs.Collection.Set]
pop [Sigs.Collection.Map]
port [Options]
External port
pow [Sigs.Arithmetic]
power [Bigint]
power_big [Bigint]
power_big_int_positive_big_int [Bigint]
power_big_int_positive_int [Bigint]
power_int_positive_big_int [Bigint]
power_int_positive_int [Bigint]
pp [Colors]
pp ppf color is pp_with_prefix "#" ppf color
pp [Machine.Gettable_settable]
pp [Machine]
pp ppf arch pretty-prints an arch value into ppf
pp [Lreader]
pp [Disasm_types.Mnemonic]
pp [Union_find.Make]
pp [Smt_model]
pp [Sigs.Printable]
pp [Region_bitvector]
pp [Interval.S]
pp [Disasm.Program]
pp [Dba_types.AddressStack]
pp [Bitvector]
pp ppf bv prints the decimal value of bv into ppf
pp [Basic_types.Size]
pp_as_string [Print_utils]
pp_base [Dba_types.Caddress]
pp_base caddr only print the base address of the DBA code address as hexadecimal, thus ignoring the id part
pp_binary_op [Dba_printer.DbaPrinter]
pp_byte [X86pp]
pp_byte ppf v is pp_bytes 1 ppf v
pp_byte [Print_utils]
pp_byte prefixed ppf by prints as hexadecimal byte by into ppf If prefixed is true (default) it also prepends "0x".
pp_bytes [X86pp]
pp_bytes n ppf v prints the first n bytes of v into ppf.
pp_code_address [Dba_printer.DbaPrinter]
pp_cond [Dba_printer.DbaPrinter]
pp_current [Machine.Gettable_settable]
pp_dba_prelude [Print_utils]
pp_expr [Dba_printer.DbaPrinter]
pp_hex [Bitvector]
pp_hex ppf bv prints the hexadecimal value of bv into ppf
pp_hex [Basic_types.Size]
pp_instr [X86pp]
pp_instruction [Dba_printer.DbaPrinter]
pp_lhs [Dba_printer.DbaPrinter]
pp_list [Print_utils]
pp_loader_summary [Loader_utils]
pp_mnemonic [Disasm_types.BasicInstruction]
pp_opcode [Disasm_types.BasicInstruction]
pp_opt [Print_utils]
pp_opt_as_string [Print_utils]
pp_region [Dba_printer.DbaPrinter]
pp_result [Smtlib2]
pp_smt_result [Smtlib2print]
pretty print the smt_result with a given color
pp_stat_formula [Formula]
print the logical store of a formula (all the variables)
pp_tag [Dba_printer.DbaPrinter]
pp_to_file [Binpatcher.WritableLoader]
pp_to_file ~filename w writes the contents of the image to the file filename
pp_to_file [Print_utils]
pp_unary_op [Dba_printer.DbaPrinter]
pp_unknown_instructions [X86toDba]
pp_with_prefix [Colors]
pp_word [X86pp]
pp_word ppf v is pp_bytes 4 ppf v
pred [Bitvector.Common]
pred [Basic_types.Size]
pred_big_int [Bigint]
prepend_int [Basic_types.Binstream]
prepend_int64 [Basic_types.Binstream]
pretty [Llvm_decoder]
print [Union_find.Make]
print [Dba_types.Instruction]
print [Bitvector]
print_policy [Policy_engine]
print_trace [Trace_loader]
print the whole trace
process_child [Dse.DSE]
process_input [Dse.DSE]
program [Parse_helpers.Mk]
propagate_cst [Formula_optim]
propagate_cst_abv [Formula_optim]
propagate_cst_bv [Formula_optim]
pruning [Options]
Either to apply the backward pruning phase when generating a formula (default true)
pumpkin [Colors.FlatUI]
push [Solver]
send the push command to the solver

qed_check_entry [Qed]
check the given entry
qed_get_status [Qed]
return the final status after all the entries have been provided to the checker.
quiet [Logger.S]
quomod_big_int [Bigint]

random_seed [Options]
read [X86decoder]
read [Concrete_eval]
read_dba_file [Binsec_utils]
read_file [Binsec_utils]
read_modrm [X86Util]
read_modrm_xmm [X86Util]
read_optional_config_file [Binsec_utils]
read_optional_config_file optfile parses optfile if it is not None.
read_over_write [Formula_optim]
read_over_write_abv [Formula_optim]
read_over_write_bv [Formula_optim]
read_over_write_hybrid [Formula_optim]
read_over_write_hybrid_abv [Formula_optim]
read_over_write_hybrid_bv [Formula_optim]
read_raw_policy [Policy_engine]
read_rm16_with_spare [X86Util]
read_rm8_with_spare [X86Util]
readlines [File_utils]
readlines filename return the list of the lines of the complete text of the file filename
rebase [Dba_types.Caddress]
rebase_abvexpr [Formula_optim]
rebase_bvexpr [Formula_optim]
rebase_expr [Formula_optim]
recursive [Disasm_core.Successors]
reduce [Bitvector.Common]
refine [Union_find.Make]
reg16_to_string [X86Util]
reg32_to_string [X86Util]
reg32_to_string_16 [X86Util]
reg32_to_string_8 [X86Util]
reg8_to_int [X86Util]
reg8_to_string [X86Util]
reg_to_extract [X86Util]
region_equal [Region_bitvector]
region_of [Region_bitvector]
registers [Smt_model]
get_register model gets the list of registers of this model
reid [Dba_types.Caddress]
remove [Worklist.S]
remove [Union_find.Make]
remove [Dba_types.Block]
remove_char [String_utils]
remove_char c s creates a copy of s without any occurrence of c
remove_goto [Simplification_dba_prog]
remove_mustkill_lfp [Simplification_dba_prog]
remove_newline [String_utils]
remove_newline s creates a copy of s without the newline character '\n'
remove_syntax_overlaps [Union_find.Make]
replace_chars [String_utils]
replace_chars f s creates a new string where all characters c from s have been replaced by the result of f c
replace_memory [Formula_utils]
replace_memory addr data env perform a store operation of every bytes of data starting at addr
replace_register [Formula_utils]
replace the register value with the given smt_bv_expr
request_dispatcher [Server_callback]
request_dispatcher socket cmd data Dispatch the given request to the appropriate handler.
reset_successor [Dba_types.Instruction]
resize [Dba_types.LValue]
resize bitsize lv patches the lvalue lv and gives it a size of bitsize.
restrict [Region_bitvector]
restrict [Dba_types.LValue]
restrict [Dba_types.Expr]
restrict e off1 off2 creates Dba.ExprRestrict(e, off1, off2) if off2 >= off1 && off1 >=0 .
restrict_to_bit [Dba_types.LValue]
restrict_to_bit [Dba_types.Expr]
restrict_to_bit e o is restrict e o o
restricted [Parse_helpers.Mk.Expr]
result [Logger.S]
For important results that will be displayed
result_channel [Logger.S]
retrieve_comparison [High_level_predicate]
return [Generic_decoder_sig.Monad]
rev_flatten [List_utils]
rev_flatten l reverses and flatten the list of list l at the same time.
reverse [String_utils]
reverse s creates a new reversed version of s
rewind [Lreader]
rewind r n moves back the cursor n bytes.
rgb [Colors]
rotate_left [Sigs.Bitwise]
rotate_left [Region_bitvector]
rotate_left [Interval.S]
rotate_left [Dba_types.Expr]
rotate_op_to_string [X86Util]
rotate_right [Sigs.Bitwise]
rotate_right [Region_bitvector]
rotate_right [Interval.S]
rotate_right [Dba_types.Expr]
rshiftS [Region_bitvector]
rshiftU [Region_bitvector]
run [Disasm_cfg]
run [Binpatcher]
Run the binary patcher on patch file Binpatcher_options.PatchFile for the given executable.
run [Simulate]
run ~dba_file ~configuration_file () launches a simulation run using the ** DBA description in dba_file augmented by stubs and configurations from ** configuration_file *
run [Disasm]
Run disassembly with stubs from configuration_file
run [Ai]

scale_to_size [X86Util]
scale_to_string [X86Util]
score_alloc [Options]
score_file [Options]
score_free [Options]
score_use [Options]
sdiv [Sigs.Arithmetic]
sdiv [Dba_types.Expr]
section_slice [Loader_utils]
segment_reg_to_string [X86Util]
select [Generic_decoder_sig.Expr_Input]
select_child [Dse.DSE]
serialize_int64_list [Libcall_utils]
serialize_stack_params [Libcall_types.LibCall]
serialize_stack_params [Libcall_stubs]
set [Machine.Gettable_settable]
set [Simulate_options.ConditionalStrategy]
set [Options.ExecFile]
set [Disasm_options.DisassemblyMode]
set [Parameters.Generic]
set_allowed_jumpzones [Infos]
set_amd64 [Machine]
AMD64 and LittleEndian
set_arch [Loader_utils]
set_arm [Machine]
ARM with chosen endianness.
set_arm_big [Machine]
set_arm_little [Machine]
set_bit [Bitvector.Common]
set_byte_wise_linear [Disasm_options.DisassemblyMode]
set_color [Logger.S]
Activate color tags rendering on all outputs.
set_criteria [Dse.DSE]
set_dba_block [Disasm_types.Instruction]
set_debug_level [Logger.S]
set_endianness [Dba_types]
set_entry_points [Infos]
set_epilog [Call_convention.CallConvention]
set_extended_linear [Disasm_options.DisassemblyMode]
set_file [Disasm_options]
set_global_widening_delay [Infos]
set_global_widening_thresholds [Infos]
set_hi [Interval.S]
set_info_level [Logger.S]
set_instruction [Dba_types.Statement]
set_jumps [Infos]
set_linear [Disasm_options.DisassemblyMode]
set_linear_addresses [Infos]
set_lo [Interval.S]
set_location [Dba_types.Statement]
set_log_level [Logger.S]
Set logger to display only messages from that channel and those with higher loglevels.
set_param [Call_convention.CallConvention]
set_param_pointer [Call_convention.CallConvention]
set_powerpc [Machine]
PowerPC and BigEndian
set_prepend_stubs [Infos]
set_recursive [Disasm_options.DisassemblyMode]
set_ret [Call_convention.CallConvention]
set_score [Dse.DSE]
set_stops [Infos]
set_substitute_stubs [Infos]
set_successor [Dba_types.Instruction]
set_tagged_entry [Logger.S]
set_tagged_entry Print channel identifiers, like warning for the warning channel, in front of messages to explicit their origins.
set_unknown [Machine]
No architecture and LittleEndian.
set_var [Generic_decoder_sig.Instr_Input]
set_virtual_cursor [Lreader]
set_warning_level [Logger.S]
set_x86 [Machine]
X86 and LittleEndian
set_zmq_logging_only [Logger]
set_zmq_logging_only ~send b identity diverts all formatting to an identity if b is true.
sext [Dba_types.Expr]
sge [Sigs.Comparisons]
sge [Interval.S]
sge [Dba_types.Expr]
sgt [Sigs.Comparisons]
sgt [Interval.S]
sgt [Dba_types.Expr]
shift_left [Sigs.Bitwise]
shift_left [Interval.S]
shift_left [Dba_types.Expr]
shift_left_big_int [Bigint]
shift_op_to_string [X86Util]
shift_right [Sigs.Bitwise]
shift_right [Interval.S]
shift_right [Dba_types.Expr]
shift_right_big_int [Bigint]
shift_right_signed [Sigs.Bitwise]
shift_right_signed [Interval.S]
shift_right_signed [Dba_types.Expr]
shift_right_towards_zero_big_int [Bigint]
shiftd_op_to_string [X86Util]
sign_big_int [Bigint]
signed_extension [Region_bitvector]
signed_of [Bitvector.Common]
silver [Colors.FlatUI]
simpl [Disasm_options]
simpl_fun [Disasm_options]
simpl_inline_calls [Disasm_options]
simpl_no_summaries [Disasm_options]
simpl_sequence [Disasm_options]
simplification_cli_handler [Disasm_options]
Sets variables below according to command line
simplify_dba [Simplification_dba]
simplify_expr [Simplification_dba_instr]
simplify_instruction [Simplification_dba_instr]
single_thread_server_loop [Server]
Start the ZMQ-based server
singleton [Worklist.S]
singleton [Dba_types.Block]
size_abvexpr [Smtlib2]
size_bvexpr [Smtlib2]
size_of [Region_bitvector]
size_of [Dba_types.Expr]
size_of [Bitvector.Common]
size_of_hexstring [String_utils]
size_of_hexstring s computes the size in bits of hexadecimal string s.
sized_region [Parse_helpers.Mk.Expr]
sle [Sigs.Comparisons]
sle [Interval.S]
sle [Dba_types.Expr]
slt [Sigs.Comparisons]
slt [Interval.S]
slt [Dba_types.Expr]
smax [Bitvector.Common]
smin [Interval.Signed]
smin [Bitvector.Common]
smod [Sigs.Arithmetic]
smod [Dba_types.Expr]
smtBvExprAlt_to_smtBvExpr [Smt_bitvectors]
smtBvExpr_to_hstring [Smt_bitvectors]
smtBvExpr_to_string [Smt_bitvectors]
smt_functions [Smtlib2print]
smt_header [Smtlib2print]
smt_result_to_exit_code [Smtlib2]
associate an exit code for the different smt_result: SAT: 0, UNSAT: 10, TIMEOUT: 11, UNKNOWN: 12
smtabvexpr_to_string [Smtlib2print]
see smtbvexpr_to_string
smtbv_add_int [Smtlib2]
add the given int value to the expression
smtbv_add_one [Smtlib2]
add one to the given smt_bv_expr
smtbv_extract [Smtlib2]
smtbv_extract low high create an extract expression extracting from low to high bits
smtbv_sub_one [Smtlib2]
decrement the given smt_bv_expr by the constant 1
smtbvbinary_to_string [Smtlib2print]
smtbvexpr_to_string [Smtlib2print]
smtbvunary_to_string [Smtlib2print]
smtexpr_is_true [Smtlib2]
return true only if the smt_expr is SmtTrue
smtexpr_to_string [Smtlib2print]
see smtbvexpr_to_string
smtres_to_string [Smtlib2print]
smtvarset_to_string [Smtlib2print]
smul [Sigs.Arithmetic]
smul [Dba_types.Expr]
snoc [Worklist.CMake]
snoc e h inserts e at the rear of the worklist h
solve [Solver]
solve ~timeout file solver solve the formula in file with the given ~timeout and the given solver.
solve_incremental [Solver]
solve_incremental ~expr ~debug session solver solve the current formula fed to the solver.
solve_incremental_model [Solver]
same as solve_incremental_model but also returns the model generated
solve_incremental_model_time [Solver]
same as solve_incremental_model but also returns the computation time
solve_incremental_value [Solver]
same as solve_incremental_model but uses the smtlib2 get-value rather than get-model
solve_model [Solver]
same as solve but also returns the model generated
solve_model_time [Solver]
same as solve_model but also returns the computation time
sqrt_big_int [Bigint]
square_big_int [Bigint]
srem [Sigs.Arithmetic]
sse_to_string [X86Util]
st_of [Region_bitvector]
start [Dba_types.Block]
start b is the first index of block b
start_interactive [Solver]
start_interactive ~file ~timeout solver starts an interactive session with the solver solver and the given ~timeout (default is none).
static_inner_jump [Dba_types.Instruction]
static_jump [Predba]
static_jump [Dba_types.Instruction]
statistics [Simplification_dba_utils]
stop [Predba]
stop [Disasm_types.Instruction]
stop [Dba_types.Instruction]
stop_interactive [Solver]
stop the interactive session by closing the process
store [Generic_decoder_sig.Instr_Input]
store [Parse_helpers.Mk.Lhs]
store [Dba_types.LValue]
store_memory [Formula]
store_memory ~constraints abv_expr add a new store in memory add optionally attach some additional ~constraints constraints to it
strategy [Options]
string_from_pp [Print_utils]
string_of_big_int [Bigint]
string_of_digit_char [Dba_printer.Renderer]
string_of_register_restrict [X86Util]
string_to_big_int [Decode_utils]
string_to_hex [Decode_utils]
string_to_int_list [Decode_utils]
sub [Sigs.Arithmetic]
sub [Dba_types.Expr]
sub [Basic_types.Size]
sub [Basic_types.Natural]
sub_big_int [Bigint]
sub_int [Basic_types.Natural]
substitute_dba_expr [Dba_utils]
substitute_dba_expr_cond [Dba_utils]
succ [Region_bitvector]
succ [Bitvector.Common]
succ_big_int [Bigint]
successors [Disasm_core.Iterable]
successors [Dba_types.Instruction]
Properties and computations
summary_only [Options]
sunflower [Colors.FlatUI]
symbolize_and_then_concretize_register [Formula_utils]
symbolize the register and then concretize it.
symbolize_memory [Formula_utils]
symbolize_memory dba_addr prefix ~i size env symbolize the memory starting at the address dba_addr up to size.
symbolize_memory_one_octet [Formula_utils]
symbolize_memory_one_octet addr prefix env symbolize the the byte at address addr and prefix the new input symbol by prefix
symbolize_register [Formula_utils]
symbolize_register name ~is_full_name prefix create a new symbol and assign it in the register name.

take [List_utils]
take n l returns up to the n first elements of list l
temp [Dba_types.LValue]
temp n creates a lvalue representing a temporary of size n with name Format.sprintf "temp%d" n.
temp [Dba_types.Expr]
temp n creates an expression representing a temporary of size n with name Format.sprintf "temp%d" n.
temporaries [Dba_types.Instruction]
temporaries t returns a couple defined * used representing sets of temporaries being defined and used
temporary [Dba_types.LValue]
temporary [Dba_types.Expr]
temporary name nbits constructs a variable named name of size nbits flagged as a temporary
test_reg_to_string [X86Util]
time [Utils]
time f times the execution of function f and returns both the time taken and the result
time_analysis [Options]
time_disas [Options]
time_equalities [Options]
time_nat_flag_recovery [Options]
time_redundant_evals [Options]
time_simpl [Options]
to_bigint [Dba_types.Virtual_address]
to_bitsize [Basic_types.ByteSize]
to_bool [Bitvector]
to_bool [Basic_types.Ternary]
to_bool t translates a ternary value to its boolean equivalent.
to_code_address [Dba_types.Virtual_address]
to_dbainstrs [Dba_types.Block]
to_generic_instruction [X86Instruction]
to_generic_instruction [Disasm_types.Instruction]
to_hexstring [Bitvector]
to_int [Basic_types.Size]
to_int32 [Bitvector]
to_int64 [Dba_types.Virtual_address]
to_int64 [Bitvector]
to_list [Dba_types.Block]
to_pmap [Disasm_types.Program]
to_string [Disasm_types.Mnemonic]
to_string [Union_find.Make]
to_string [Simulate_options.SemanticsMode]
to_string [Region_bitvector]
to_string [Libcall_types.LibCall]
to_string [Basic_types.Binstream]
to_stringmap [Formula_type]
top [Interval.S]
topify [Interval.S]
trace_limit_length [Options]
true_ [Transfer_functions.Boolean_Forward]
turquoise [Colors.FlatUI]

u16 [Lreader.Accessor]
u32 [Lreader.Accessor]
u64 [Lreader.Accessor]
u8 [Lreader.Accessor]
udiv [Sigs.Arithmetic]
udiv [Dba_types.Expr]
uext [Dba_types.Expr]
uge [Sigs.Comparisons]
uge [Interval.S]
uge [Dba_types.Expr]
ugt [Sigs.Comparisons]
ugt [Interval.S]
ugt [Dba_types.Expr]
ule [Sigs.Comparisons]
ule [Interval.S]
ule [Dba_types.Expr]
ult [Sigs.Comparisons]
ult [Interval.S]
ult [Dba_types.Expr]
umax [Bitvector.Common]
umin [Bitvector.Common]
uminus [Dba_types.Expr]
umod [Sigs.Arithmetic]
umod [Dba_types.Expr]
umul [Sigs.Arithmetic]
umul [Dba_types.Expr]
unary [Dba_types.Expr]
unary [Dba_to_smtlib]
convert a DBA unary operator to a Smtlib unary operator
unary_ops [Dba_printer.Renderer]
undef [Generic_decoder_sig.Instr_Input]
undefined [Predba]
undefined [Region_bitvector]
undefined n creates an undefined value of bitsize n
undefined [Dba_types.Instruction]
unhandled [Disasm_types.Mnemonic]
union [Union_find.Make]
unit_big_int [Bigint]
unknown [Generic_decoder_sig.Instr_Input]
unknown_instructions [X86toDba]
insertions / unique insertions
unroll_current_loop [Ai_utils]
unrolled_loops_at_address [Ai_utils]
unsafe_bitsize [Dba_types.LValue]
unsafe_get_opt [Utils]
unsafe_get_opt vopt retrieves the contents of vopt.
update_flags [High_level_predicate]
update_hybrid_memory [Formula_optim]
update_instr_map [Static_utils]
urem [Sigs.Arithmetic]

value_of [Region_bitvector]
value_of [Bitvector.Common]
values [Sigs.Collection.Map]
var [Dba_types.LValue]
var name size tagopt creates a DBA lvalue for a variable
var [Dba_types.Expr]
variables [Dba_types.Instruction]
variables t returns a couple defined * used representing sets of variable names defined and used at instruction t
vhex [Parse_helpers.Message.Value]
vint [Parse_helpers.Message.Value]
violated_call_ret_file [Options]
Call stack tampering information file (for assisted disassembly
vstr [Parse_helpers.Message.Value]

warning [Logger.S]
For warning messages.
warning_channel [Logger.S]
wetasphalt [Colors.FlatUI]
widen [Union_find.Make]
wisteria [Colors.FlatUI]
with_tags_on [Logger]
with_tags_on ppf fmt pretty-prints fmt on the pretty-printing formatter ppf with tag marking and printing functions activated.
write [Concrete_eval]

xmm_reg_to_mm_reg [X86Util]
xmm_reg_to_string [X86Util]
xor_big_int [Bigint]

yices_extract [Smt_model]
yices_extract s extracts the same information as extract but for a ** yices-smt2 produced model ** yices-smt2 models use another syntax and are parsed on their own ** s is expected to be the raw string of the model and not, for example, a ** filename

zero [Smtlib2]
zero [Dba_types.Expr]
zero [Bitvector.Common]
zero_big_int [Bigint]
zeros [Region_bitvector]
zeros size creates a bitvector of value 0 with size size in region `Constant
zeros [Dba_types.Expr]
zeros n creates a constant expression of value 0 with length n
zeros [Bitvector.Common]