cprover
|
#include <goto_functions_template.h>
Public Types | |
typedef goto_function_templatet< bodyT > | goto_functiont |
typedef std::map< irep_idt, goto_functiont > | function_mapt |
Public Member Functions | |
goto_functions_templatet () | |
goto_functions_templatet (const goto_functions_templatet &)=delete | |
goto_functions_templatet & | operator= (const goto_functions_templatet &)=delete |
goto_functions_templatet (goto_functions_templatet &&other) | |
goto_functions_templatet & | operator= (goto_functions_templatet &&other) |
void | clear () |
void | output (const namespacet &ns, std::ostream &out) const |
void | compute_location_numbers () |
void | compute_loop_numbers () |
void | compute_target_numbers () |
void | compute_incoming_edges () |
void | update () |
void | swap (goto_functions_templatet &other) |
void | copy_from (const goto_functions_templatet &other) |
Static Public Member Functions | |
static irep_idt | entry_point () |
Public Attributes | |
function_mapt | function_map |
Definition at line 99 of file goto_functions_template.h.
typedef std::map<irep_idt, goto_functiont> goto_functions_templatet< bodyT >::function_mapt |
Definition at line 103 of file goto_functions_template.h.
typedef goto_function_templatet<bodyT> goto_functions_templatet< bodyT >::goto_functiont |
Definition at line 102 of file goto_functions_template.h.
|
inline |
Definition at line 106 of file goto_functions_template.h.
|
delete |
|
inline |
Definition at line 113 of file goto_functions_template.h.
|
inline |
Definition at line 124 of file goto_functions_template.h.
Referenced by goto_modelt::clear(), compilet::compile(), and compilet::doit().
void goto_functions_templatet< bodyT >::compute_incoming_edges | ( | ) |
Definition at line 197 of file goto_functions_template.h.
Referenced by goto_functions_templatet< goto_programt >::update().
void goto_functions_templatet< bodyT >::compute_location_numbers | ( | ) |
Definition at line 185 of file goto_functions_template.h.
Referenced by goto_convert_functionst::goto_convert(), remove_instanceoft::lower_instanceof(), remove_virtual_functionst::operator()(), remove_function_pointerst::operator()(), read_bin_goto_object_v3(), and goto_functions_templatet< goto_programt >::update().
void goto_functions_templatet< bodyT >::compute_loop_numbers | ( | ) |
Definition at line 217 of file goto_functions_template.h.
Referenced by goto_instrument_parse_optionst::doit(), goto_function_inline_and_log(), goto_fence_inserter_parse_optionst::instrument_goto_program(), goto_instrument_parse_optionst::instrument_goto_program(), clobber_parse_optionst::process_goto_program(), goto_diff_parse_optionst::process_goto_program(), symex_parse_optionst::process_goto_program(), goto_analyzer_parse_optionst::process_goto_program(), cbmc_parse_optionst::process_goto_program(), and goto_functions_templatet< goto_programt >::update().
void goto_functions_templatet< bodyT >::compute_target_numbers | ( | ) |
Definition at line 207 of file goto_functions_template.h.
Referenced by goto_functions_templatet< goto_programt >::update().
|
inline |
Definition at line 157 of file goto_functions_template.h.
|
inlinestatic |
Definition at line 146 of file goto_functions_template.h.
Referenced by shared_bufferst::add_initialization_code(), compute_called_functions(), symex_coveraget::compute_overall_coverage(), show_goto_functions_xmlt::convert(), show_goto_functions_jsont::convert(), ai_baset::entry_state(), clobber_parse_optionst::get_goto_program(), instrumentert::goto2graph_cfg(), goto_partial_inline(), property_checkert::initialize_property_map(), instrument_cover_goals(), string_abstractiont::operator()(), print_path_lengths(), race_check(), ai_baset::sequential_fixedpoint(), symex_bmct::symex_step(), and weak_memory().
|
delete |
Referenced by goto_functionst::operator=().
|
inline |
Definition at line 118 of file goto_functions_template.h.
void goto_functions_templatet< bodyT >::output | ( | const namespacet & | ns, |
std::ostream & | out | ||
) | const |
Definition at line 165 of file goto_functions_template.h.
Referenced by goto_modelt::output(), and show_goto_functions().
|
inline |
Definition at line 152 of file goto_functions_template.h.
|
inline |
Definition at line 138 of file goto_functions_template.h.
Referenced by goto_instrument_parse_optionst::doit(), const_function_pointer_propagationt::dup_caller_and_inline_callee(), fence_pensieve(), fence_weak_memory(), goto_function_inline_and_log(), instrument_cover_goals(), goto_fence_inserter_parse_optionst::instrument_goto_program(), goto_instrument_parse_optionst::instrument_goto_program(), interrupt(), mmio(), model_argc_argv(), nondet_static(), nondet_volatile(), taint_analysist::operator()(), code_contractst::operator()(), full_slicert::operator()(), clobber_parse_optionst::process_goto_program(), goto_diff_parse_optionst::process_goto_program(), goto_analyzer_parse_optionst::process_goto_program(), symex_parse_optionst::process_goto_program(), cbmc_parse_optionst::process_goto_program(), propagate_const_function_pointers(), race_check(), skip_loops(), reachability_slicert::slice(), slice_global_inits(), stack_depth(), and weak_memory().
function_mapt goto_functions_templatet< bodyT >::function_map |
Definition at line 104 of file goto_functions_template.h.
Referenced by const_function_pointer_propagationt::arg_stackt::add_args(), code_contractst::add_contract_check(), full_slicert::add_function_calls(), shared_bufferst::add_initialization_code(), change_impactt::change_impact(), goto_inlinet::check_inline_map(), goto_functions_templatet< goto_programt >::clear(), fence_all_shared_aegt::compute(), compute_called_functions(), cfg_baset< cfg_nodet >::compute_edges_function_call(), rw_set_functiont::compute_rec(), show_goto_functions_jsont::convert(), show_goto_functions_xmlt::convert(), convert(), goto_convert_functionst::convert_function(), goto_difft::convert_function(), dump_ct::convert_function_declaration(), goto_functions_templatet< goto_programt >::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(), remove_returnst::do_function_calls(), goto_instrument_parse_optionst::doit(), const_function_pointer_propagationt::dup_caller_and_inline_callee(), ai_baset::entry_state(), interpretert::execute_function_call(), goto_inlinet::expand_function_call(), fence_all_shared_aegt::fence_all_shared_aeg_explore(), find_used_functions(), compilet::function_body_count(), unified_difft::get_diff(), function_modifiest::get_modifies_function(), instrumentert::goto2graph_cfg(), goto_function_inline(), goto_function_inline_and_log(), goto_inline(), goto_partial_inline(), goto_rw(), goto_symex_statet::initialize(), taint_analysist::instrument(), instrumentert::is_cfg_spurious(), label_properties(), compilet::link(), link_functions(), link_to_library(), remove_instanceoft::lower_instanceof(), make_assertions_false(), mm_io(), model_argc_argv(), nondet_static(), remove_virtual_functionst::operator()(), syntactic_difft::operator()(), string_abstractiont::operator()(), interpretert::operator()(), taint_analysist::operator()(), code_contractst::operator()(), remove_function_pointerst::operator()(), dump_ct::operator()(), string_instrumentationt::operator()(), goto_symext::operator()(), local_may_alias_factoryt::operator()(), check_call_sequencet::operator()(), goto_functions_templatet< goto_programt >::operator=(), unified_difft::output(), change_impactt::output_change_impact(), goto_difft::output_functions(), goto_inlinet::output_inline_map(), print_path_lengths(), const_function_pointer_propagationt::propagate(), race_check(), read_bin_goto_object_v3(), read_goto_object(), remove_function(), remove_unused_functions(), ai_baset::sequential_fixedpoint(), show_locations(), show_properties(), show_properties_json(), slice_global_inits(), stack_depth(), goto_functions_templatet< goto_programt >::swap(), goto_symext::symex_function_call_code(), thread_exit_instrumentation(), undefined_function_abort_path(), ai_baset::visit(), shared_bufferst::cfg_visitort::weak_memory(), compilet::write_bin_object_file(), and write_goto_binary_v3().