cprover
|
#include <goto_functions.h>
Public Types | |
using | goto_functiont = ::goto_functiont |
typedef std::map< irep_idt, goto_functiont > | function_mapt |
Public Member Functions | |
goto_functionst () | |
goto_functionst (const goto_functionst &)=delete | |
goto_functionst & | operator= (const goto_functionst &)=delete |
goto_functionst (goto_functionst &&other) | |
goto_functionst & | operator= (goto_functionst &&other) |
void | unload (const irep_idt &name) |
void | clear () |
void | output (const namespacet &ns, std::ostream &out) const |
void | compute_location_numbers () |
void | compute_location_numbers (goto_programt &) |
void | compute_loop_numbers () |
void | compute_target_numbers () |
void | compute_incoming_edges () |
void | update_instructions_function () |
update the function member in each instruction by setting it to the goto function's identifier More... | |
void | update () |
void | swap (goto_functionst &other) |
void | copy_from (const goto_functionst &other) |
Static Public Member Functions | |
static irep_idt | entry_point () |
Public Attributes | |
function_mapt | function_map |
Private Attributes | |
unsigned | unused_location_number |
A location number such that numbers in the interval [unused_location_number, MAX_UINT] are all unused. More... | |
Definition at line 21 of file goto_functions.h.
typedef std::map<irep_idt, goto_functiont> goto_functionst::function_mapt |
Definition at line 25 of file goto_functions.h.
Definition at line 24 of file goto_functions.h.
|
inline |
Definition at line 37 of file goto_functions.h.
|
delete |
|
inline |
Definition at line 53 of file goto_functions.h.
|
inline |
Definition at line 68 of file goto_functions.h.
References function_map.
Referenced by goto_modelt::clear(), compilet::compile(), and compilet::doit().
void goto_functionst::compute_incoming_edges | ( | ) |
void goto_functionst::compute_location_numbers | ( | ) |
Definition at line 35 of file goto_functions.cpp.
References function_map, and unused_location_number.
Referenced by goto_model_functiont::compute_location_numbers(), convert_nondet(), goto_convert_functionst::goto_convert(), instrument_cover_goals(), remove_virtual_functionst::operator()(), remove_function_pointerst::operator()(), read_bin_goto_object_v3(), remove_instanceof(), remove_java_new(), and update().
void goto_functionst::compute_location_numbers | ( | goto_programt & | program | ) |
Definition at line 45 of file goto_functions.cpp.
References goto_programt::compute_location_numbers(), and unused_location_number.
void goto_functionst::compute_loop_numbers | ( | ) |
Definition at line 69 of file goto_functions.cpp.
References function_map.
Referenced by goto_function_inline_and_log(), goto_instrument_parse_optionst::instrument_goto_program(), clobber_parse_optionst::process_goto_program(), jdiff_parse_optionst::process_goto_program(), goto_diff_parse_optionst::process_goto_program(), cbmc_parse_optionst::process_goto_program(), janalyzer_parse_optionst::process_goto_program(), goto_analyzer_parse_optionst::process_goto_program(), and update().
void goto_functionst::compute_target_numbers | ( | ) |
|
inline |
Definition at line 113 of file goto_functions.h.
References function_map.
|
inlinestatic |
Definition at line 102 of file goto_functions.h.
References CPROVER_PREFIX.
Referenced by shared_bufferst::add_initialization_code(), ansi_c_entry_point(), c_nondet_symbol_factory(), jbmc_parse_optionst::can_generate_function_body(), compute_called_functions(), symex_coveraget::compute_overall_coverage(), dump_ct::convert_function_declaration(), jbmc_parse_optionst::doit(), goto_instrument_parse_optionst::doit(), ai_baset::entry_state(), generate_ansi_c_start_function(), generate_java_start_function(), rebuild_goto_start_function_baset< maybe_lazy_goto_modelt >::get_entry_point_mode(), instrumentert::goto2graph_cfg(), goto_checkt::goto_check(), goto_inline(), goto_partial_inline(), lazy_goto_modelt::initialize(), interpretert::initialize(), initialize_goto_model(), property_checkert::initialize_property_map(), instrument_cover_goals(), interrupt(), instrumentert::is_cfg_spurious(), java_build_arguments(), java_entry_point(), jsil_entry_point(), compilet::link(), mmio(), model_argc_argv(), object_factory(), string_abstractiont::operator()(), taint_analysist::operator()(), rebuild_goto_start_function_baset< maybe_lazy_goto_modelt >::operator()(), dump_ct::operator()(), internal_functions_filtert::operator()(), print_path_lengths(), race_check(), rebuild_goto_start_function_baset< maybe_lazy_goto_modelt >::remove_existing_entry_point(), remove_unused_functions(), require_goto_statements::require_entry_point_argument_assignment(), require_goto_statements::require_entry_point_statements(), ai_baset::sequential_fixedpoint(), slice_global_inits(), stack_depth(), goto_symext::symex_from_entry_point_of(), symex_bmct::symex_step(), update_internal_field(), and weak_memory().
|
delete |
|
inline |
Definition at line 59 of file goto_functions.h.
References function_map, and unused_location_number.
void goto_functionst::output | ( | const namespacet & | ns, |
std::ostream & | out | ||
) | const |
Definition at line 16 of file goto_functions.cpp.
References symbolt::display_name(), function_map, namespacet::lookup(), and symbolt::name.
Referenced by goto_modelt::output(), and show_goto_functions().
|
inline |
Definition at line 108 of file goto_functions.h.
References function_map.
Referenced by read_object_and_link().
|
inline |
Definition at line 66 of file goto_functions.h.
References function_map.
Referenced by goto_modelt::unload().
|
inline |
Definition at line 93 of file goto_functions.h.
References compute_incoming_edges(), compute_location_numbers(), compute_loop_numbers(), compute_target_numbers(), and update_instructions_function().
Referenced by goto_instrument_parse_optionst::doit(), goto_function_inline_and_log(), goto_instrument_parse_optionst::instrument_goto_program(), interrupt(), mmio(), nondet_static(), nondet_volatile(), taint_analysist::operator()(), code_contractst::operator()(), jbmc_parse_optionst::process_goto_functions(), clobber_parse_optionst::process_goto_program(), jdiff_parse_optionst::process_goto_program(), goto_diff_parse_optionst::process_goto_program(), cbmc_parse_optionst::process_goto_program(), janalyzer_parse_optionst::process_goto_program(), goto_analyzer_parse_optionst::process_goto_program(), race_check(), remove_skip(), skip_loops(), splice_call(), stack_depth(), static_simplifier(), and weak_memory().
|
inline |
update the function member in each instruction by setting it to the goto function's identifier
Definition at line 85 of file goto_functions.h.
References function_map.
Referenced by update().
function_mapt goto_functionst::function_map |
Definition at line 26 of file goto_functions.h.
Referenced by code_contractst::add_contract_check(), full_slicert::add_function_calls(), shared_bufferst::add_initialization_code(), linker_script_merget::add_linker_script_definitions(), call_grapht::call_grapht(), goto_modelt::can_produce_function(), wrapper_goto_modelt::can_produce_function(), change_impactt::change_impact(), goto_inlinet::check_inline_map(), clear(), compute_called_functions(), cfg_baset< cfg_nodet >::compute_edges_function_call(), compute_incoming_edges(), compute_location_numbers(), compute_loop_numbers(), rw_set_functiont::compute_rec(), compute_target_numbers(), show_goto_functions_jsont::convert(), show_goto_functions_xmlt::convert(), convert(), dump_ct::convert_function_declaration(), goto_difft::convert_function_json(), convert_nondet(), compilet::convert_symbols(), copy_from(), goto_program_dereferencet::dereference_program(), flow_insensitive_analysis_baset::do_function_call_rec(), static_analysis_baset::do_function_call_rec(), ai_baset::do_function_call_rec(), goto_instrument_parse_optionst::doit(), ai_baset::entry_state(), interpretert::execute_function_call(), goto_inlinet::expand_function_call(), find_property(), find_used_functions(), compilet::function_body_count(), generate_function_bodies(), unified_difft::get_diff(), get_function_from_goto_functions(), goto_modelt::get_goto_function(), wrapper_goto_modelt::get_goto_function(), function_modifiest::get_modifies_function(), get_preconditions(), instrumentert::goto2graph_cfg(), goto_convert(), goto_convert_functionst::goto_convert(), goto_function_inline(), goto_function_inline_and_log(), goto_inline(), goto_partial_inline(), goto_rw(), interpretert::initialize(), taint_analysist::instrument(), instrument_cover_goals(), instrument_preconditions(), instrumentert::is_cfg_spurious(), remove_calls_no_bodyt::is_opaque_function_call(), label_properties(), compilet::link(), link_functions(), link_to_library(), make_assertions_false(), mm_io(), model_argc_argv(), nondet_static(), java_syntactic_difft::operator()(), remove_virtual_functionst::operator()(), syntactic_difft::operator()(), string_abstractiont::operator()(), remove_returnst::operator()(), taint_analysist::operator()(), code_contractst::operator()(), remove_function_pointerst::operator()(), dump_ct::operator()(), string_instrumentationt::operator()(), check_call_sequencet::operator()(), local_may_alias_factoryt::operator()(), operator=(), unified_difft::output(), output(), change_impactt::output_change_impact(), goto_difft::output_function(), goto_inlinet::output_inline_map(), linker_script_merget::pointerize_linker_defined_symbols(), print_global_state_size(), print_path_lengths(), race_check(), read_bin_goto_object_v3(), remove_asm(), remove_function(), remove_instanceof(), remove_java_new(), remove_unused_functions(), replace_java_nondet(), ai_baset::sequential_fixedpoint(), show_goto_functions(), show_locations(), show_properties(), show_properties_json(), slice_global_inits(), splice_call(), stack_depth(), swap(), thread_exit_instrumentation(), undefined_function_abort_path(), unload(), update_instructions_function(), ai_baset::visit(), shared_bufferst::cfg_visitort::weak_memory(), compilet::write_bin_object_file(), and write_goto_binary_v3().
|
private |
A location number such that numbers in the interval [unused_location_number, MAX_UINT] are all unused.
There might still be unused numbers below this. If numbering a new function or renumbering a function, starting from this number is safe.
Definition at line 34 of file goto_functions.h.
Referenced by compute_location_numbers(), and operator=().