cprover
goto_functions.h File Reference

Goto Programs with Functions. More...

#include "goto_function.h"
#include <util/cprover_prefix.h>
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)
 

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 125 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(), dirtyt::build(), call_grapht::call_grapht(), custom_bitvector_analysist::check(), goto_inlinet::check_inline_map(), goto_checkt::collect_allocations(), collect_eloc(), uncaught_exceptions_analysist::collect_uncaught_exceptions(), is_threadedt::compute(), compute_address_taken_functions(), compute_called_functions_from_ai(), cfg_baset< cfg_nodet >::compute_edges(), symex_coveraget::compute_overall_coverage(), static_analysis_baset::concurrent_fixedpoint(), ai_baset::concurrent_fixedpoint(), 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(), concurrency_instrumentationt::instrument(), list_calls_and_arguments(), list_functions(), list_undefined_functions(), syntactic_difft::operator()(), java_syntactic_difft::operator()(), bmc_all_propertiest::operator()(), unified_difft::operator()(), taint_analysist::operator()(), bmc_covert::operator()(), local_may_alias_factoryt::operator()(), change_impactt::operator()(), dott::output(), uncaught_exceptions_analysist::output(), flow_insensitive_analysis_baset::output(), static_analysis_baset::output(), ai_baset::output(), ai_baset::output_json(), ai_baset::output_xml(), janalyzer_parse_optionst::perform_analysis(), goto_analyzer_parse_optionst::perform_analysis(), 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(), static_unreachable_instructions(), static_verifier(), thread_exit_instrumentation(), unreachable_instructions(), static_analysis_baset::update(), and write_goto_binary_v3().