CBMC
memory_snapshot_harness_generatort Member List

This is the complete list of members for memory_snapshot_harness_generatort, including all inherited members.

add_assignments_to_globals(const symbol_table_baset &snapshot, goto_modelt &goto_model) constmemory_snapshot_harness_generatortprotected
add_call_with_nondet_arguments(const symbolt &called_function_symbol, code_blockt &code) constmemory_snapshot_harness_generatortprotected
add_init_section(const symbol_exprt &func_init_done_var, goto_modelt &goto_model) constmemory_snapshot_harness_generatortprotected
collect_references(const exprt &expr, Adder &&add_reference) constmemory_snapshot_harness_generatortinlineprotected
entry_locationmemory_snapshot_harness_generatortprotected
fresh_symbol_copy(const symbolt &snapshot_symbol, symbol_table_baset &symbol_table) constmemory_snapshot_harness_generatortprotected
generate(goto_modelt &goto_model, const irep_idt &harness_function_name) overridememory_snapshot_harness_generatortvirtual
get_memory_snapshot(const std::string &file, symbol_table_baset &snapshot) constmemory_snapshot_harness_generatortprotected
handle_option(const std::string &option, const std::list< std::string > &values) overridememory_snapshot_harness_generatortprotectedvirtual
initial_goto_location_linememory_snapshot_harness_generatortprotected
initial_source_location_linememory_snapshot_harness_generatortprotected
initialize_entry_via_goto(const entry_goto_locationt &entry_goto_location, const goto_functionst &goto_functions)memory_snapshot_harness_generatortprotected
initialize_entry_via_source(const entry_source_locationt &entry_source_location, const goto_functionst &goto_functions)memory_snapshot_harness_generatortprotected
insert_harness_function_into_goto_model(goto_modelt &goto_model, const symbolt &function) constmemory_snapshot_harness_generatortprotected
memory_snapshot_filememory_snapshot_harness_generatortprotected
memory_snapshot_harness_generatort(message_handlert &message_handler)memory_snapshot_harness_generatortinlineexplicit
message_handlermemory_snapshot_harness_generatortprotected
parse_goto_location(const std::string &cmdl_option)memory_snapshot_harness_generatortprotected
parse_source_location(const std::string &cmdl_option)memory_snapshot_harness_generatortprotected
pointer_depth(const typet &t) constmemory_snapshot_harness_generatortprotected
recursive_initialization_configmemory_snapshot_harness_generatortprotected
validate_options(const goto_modelt &goto_model) overridememory_snapshot_harness_generatortprotectedvirtual
variables_to_havocmemory_snapshot_harness_generatortprotected
~goto_harness_generatort()=defaultgoto_harness_generatortvirtual