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) |
Goto Programs with Functions.
Definition in file goto_functions.h.
#define Forall_goto_functions | ( | it, | |
functions | |||
) |
Definition at line 120 of file goto_functions.h.
Referenced by accelerate_functions(), add_uninitialized_locals_assertions(), adjust_float_expressions(), shared_bufferst::affected_by_delay(), branch(), 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_calls_no_bodyt::operator()(), code_contractst::operator()(), full_slicert::operator()(), goto_unwindt::operator()(), remove_exceptionst::operator()(), race_check(), remove_complex(), remove_pointers(), remove_skip(), remove_unreachable(), remove_vector(), constant_propagator_ait::replace(), remove_returnst::restore(), rewrite_union(), set_properties(), invariant_propagationt::simplify(), skip_loops(), reachability_slicert::slice(), stack_depth(), static_simplifier(), undefined_function_abort_path(), and weak_memory().
#define forall_goto_functions | ( | it, | |
functions | |||
) |
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(), aggressive_slicert::doit(), document_propertiest::doit(), goto_instrument_parse_optionst::doit(), aggressive_slicert::find_functions_that_contain_name_snippet(), 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(), ai_baset::output(), flow_insensitive_analysis_baset::output(), static_analysis_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().