cprover
|
Goto Programs with Functions. More...
Go to the source code of this file.
Classes | |
class | goto_functionst |
Macros | |
#define | Forall_goto_functions(it, functions) |
#define | forall_goto_functions(it, functions) |
Functions | |
void | get_local_identifiers (const goto_function_templatet< goto_programt > &goto_function, std::set< irep_idt > &dest) |
Goto Programs with Functions.
Definition in file goto_functions.h.
#define Forall_goto_functions | ( | it, | |
functions | |||
) |
Definition at line 48 of file goto_functions.h.
Referenced by accelerate_functions(), add_uninitialized_locals_assertions(), adjust_float_expressions(), shared_bufferst::affected_by_delay(), branch(), fence_pensieve(), fence_weak_memory(), function_enter(), function_exit(), goto_check(), goto_inline(), goto_inlinet::goto_inline(), goto_partial_inline(), havoc_loops(), concurrency_instrumentationt::instrument(), escape_analysist::instrument(), instrument_cover_goals(), interrupt(), interval_analysis(), instrumentert::is_cfg_spurious(), k_induction(), link_functions(), mmio(), mutex_init_instrumentation(), nondet_volatile(), parameter_assignmentst::operator()(), remove_returnst::operator()(), string_abstractiont::operator()(), remove_asmt::operator()(), code_contractst::operator()(), remove_exceptionst::operator()(), full_slicert::operator()(), goto_unwindt::operator()(), race_check(), remove_complex(), remove_pointers(), remove_skip(), remove_unreachable(), remove_vector(), constant_propagator_ait::replace(), replace_async(), remove_returnst::restore(), rewrite_union(), set_properties(), invariant_propagationt::simplify(), skip_loops(), reachability_slicert::slice(), stack_depth(), undefined_function_abort_path(), and weak_memory().
#define forall_goto_functions | ( | it, | |
functions | |||
) |
Definition at line 53 of file goto_functions.h.
Referenced by invariant_propagationt::add_objects(), value_set_analysis_fit::add_vars(), value_set_analysis_fivrt::add_vars(), value_set_analysis_fivrnst::add_vars(), locst::build(), call_grapht::call_grapht(), custom_bitvector_analysist::check(), goto_inlinet::check_inline_map(), goto_checkt::collect_allocations(), collect_eloc(), is_threadedt::compute(), fence_all_sharedt::compute(), fence_volatilet::compute(), compute_address_taken_functions(), cfg_baset< cfg_nodet >::compute_edges(), symex_coveraget::compute_overall_coverage(), static_analysis_baset::concurrent_fixedpoint(), ai_baset::concurrent_fixedpoint(), dirtyt::dirtyt(), goto_analyzer_parse_optionst::doit(), document_propertiest::doit(), goto_instrument_parse_optionst::doit(), flow_insensitive_analysis_baset::fixedpoint(), static_analysis_baset::generate_states(), invariant_propagationt::initialize(), ai_baset::initialize(), property_checkert::initialize_property_map(), path_searcht::initialize_property_map(), concurrency_instrumentationt::instrument(), static_analyzert::json_report(), list_calls_and_arguments(), list_functions(), list_undefined_functions(), syntactic_difft::operator()(), bmc_all_propertiest::operator()(), taint_analysist::operator()(), unified_difft::operator()(), bmc_covert::operator()(), local_may_alias_factoryt::operator()(), change_impactt::operator()(), dott::output(), flow_insensitive_analysis_baset::output(), static_analysis_baset::output(), ai_baset::output(), ai_baset::output_json(), ai_baset::output_xml(), static_analyzert::plain_text_report(), print_path_lengths(), remove_function_pointerst::remove_function_pointerst(), static_analysis_baset::sequential_fixedpoint(), show_call_sequences(), show_loop_ids(), show_natural_loops(), show_uninitialized(), thread_exit_instrumentation(), unreachable_instructions(), remove_static_init_loopst::unwind_enum_static(), static_analysis_baset::update(), write_goto_binary_v3(), and static_analyzert::xml_report().
void get_local_identifiers | ( | const goto_function_templatet< goto_programt > & | goto_function, |
std::set< irep_idt > & | dest | ||
) |
Definition at line 16 of file goto_functions.cpp.
References goto_function_templatet< bodyT >::body, goto_programt::get_decl_identifiers(), code_typet::parameters(), and goto_function_templatet< bodyT >::type.
Referenced by invariant_propagationt::add_objects(), value_set_analysis_fit::add_vars(), value_set_analysis_fivrt::add_vars(), value_set_analysis_fivrnst::add_vars(), interpretert::execute_function_call(), and goto_symext::locality().