cprover
goto_functions.h File Reference

Goto Programs with Functions. More...

Include dependency graph for goto_functions.h:

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)
 

Detailed Description

Goto Programs with Functions.

Definition in file goto_functions.h.

Macro Definition Documentation

§ Forall_goto_functions

§ forall_goto_functions

#define forall_goto_functions (   it,
  functions 
)
Value:
for(goto_functionst::function_mapt::const_iterator \
it=(functions).function_map.begin(); \
it!=(functions).function_map.end(); it++)

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().

Function Documentation

§ get_local_identifiers()