cprover
|
A generic container class for the GOTO intermediate representation of one function. More...
#include <goto_program.h>
Classes | |
class | instructiont |
This class represents an instruction in the GOTO intermediate representation. More... | |
Public Types | |
typedef std::list< instructiont > | instructionst |
typedef instructionst::iterator | targett |
typedef instructionst::const_iterator | const_targett |
typedef std::list< targett > | targetst |
typedef std::list< const_targett > | const_targetst |
typedef std::set< irep_idt > | decl_identifierst |
Public Member Functions | |
goto_programt (const goto_programt &)=delete | |
Copying is deleted as this class contains pointers that cannot be copied. More... | |
goto_programt & | operator= (const goto_programt &)=delete |
goto_programt (goto_programt &&other) | |
goto_programt & | operator= (goto_programt &&other) |
targett | const_cast_target (const_targett t) |
Convert a const_targett to a targett - use with care and avoid whenever possible. More... | |
const_targett | const_cast_target (const_targett t) const |
Dummy for templates with possible const contexts. More... | |
template<typename Target > | |
std::list< Target > | get_successors (Target target) const |
void | compute_incoming_edges () |
void | insert_before_swap (targett target) |
Insertion that preserves jumps to "target". More... | |
void | insert_before_swap (targett target, instructiont &instruction) |
Insertion that preserves jumps to "target". More... | |
void | insert_before_swap (targett target, goto_programt &p) |
Insertion that preserves jumps to "target". More... | |
targett | insert_before (const_targett target) |
Insertion before the given target. More... | |
targett | insert_after (const_targett target) |
Insertion after the given target. More... | |
void | destructive_append (goto_programt &p) |
Appends the given program, which is destroyed. More... | |
void | destructive_insert (const_targett target, goto_programt &p) |
Inserts the given program at the given location. More... | |
targett | add_instruction () |
Adds an instruction at the end. More... | |
targett | add_instruction (goto_program_instruction_typet type) |
Adds an instruction of given type at the end. More... | |
std::ostream & | output (const namespacet &ns, const irep_idt &identifier, std::ostream &out) const |
Output goto program to given stream. More... | |
std::ostream & | output (std::ostream &out) const |
Output goto-program to given stream. More... | |
std::ostream & | output_instruction (const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &it) const |
Output a single instruction. More... | |
void | compute_target_numbers () |
Compute the target numbers. More... | |
void | compute_location_numbers (unsigned &nr) |
Compute location numbers. More... | |
void | update_instructions_function (const irep_idt &function_id) |
Sets the function member of each instruction if not yet set Note that a goto program need not be a goto function and therefore, we cannot do this in update(), but only at the level of of goto_functionst where goto programs are guaranteed to be named functions. More... | |
void | compute_location_numbers () |
Compute location numbers. More... | |
void | compute_loop_numbers () |
Compute loop numbers. More... | |
void | update () |
Update all indices. More... | |
bool | empty () const |
Is the program empty? More... | |
goto_programt () | |
Constructor. More... | |
~goto_programt () | |
void | swap (goto_programt &program) |
Swap the goto program. More... | |
void | clear () |
Clear the goto program. More... | |
targett | get_end_function () |
const_targett | get_end_function () const |
void | copy_from (const goto_programt &src) |
Copy a full goto program, preserving targets. More... | |
bool | has_assertion () const |
Does the goto program have an assertion? More... | |
void | get_decl_identifiers (decl_identifierst &decl_identifiers) const |
get the variables in decl statements More... | |
Static Public Member Functions | |
static const irep_idt | get_function_id (const_targett l) |
static const irep_idt | get_function_id (const goto_programt &p) |
static irep_idt | loop_id (const instructiont &instruction) |
Human-readable loop name. More... | |
Public Attributes | |
instructionst | instructions |
The list of instructions in the goto program. More... | |
A generic container class for the GOTO intermediate representation of one function.
A function is represented by a std::list of instructions. Execution starts in the first instruction of the list. Then, the execution of the i-th instruction is followed by the execution of the (i+1)-th instruction unless instruction i jumps to some other instruction in the list. See the internal class instructiont for additional details
Although it is straightforward to compute the control flow graph (CFG) of a function from the list of instructions and the goto target locations in instructions, the GOTO intermediate representation is not regarded as the CFG of a function. See instead the class cfg_baset, which is based on grapht and allows for easier implementation of generic graph algorithms (e.g., dominator analysis).
Definition at line 70 of file goto_program.h.
typedef std::list<const_targett> goto_programt::const_targetst |
Definition at line 400 of file goto_program.h.
typedef instructionst::const_iterator goto_programt::const_targett |
Definition at line 398 of file goto_program.h.
typedef std::set<irep_idt> goto_programt::decl_identifierst |
Definition at line 640 of file goto_program.h.
typedef std::list<instructiont> goto_programt::instructionst |
Definition at line 395 of file goto_program.h.
typedef std::list<targett> goto_programt::targetst |
Definition at line 399 of file goto_program.h.
typedef instructionst::iterator goto_programt::targett |
Definition at line 397 of file goto_program.h.
|
delete |
Copying is deleted as this class contains pointers that cannot be copied.
|
inline |
Definition at line 83 of file goto_program.h.
|
inline |
Constructor.
Definition at line 596 of file goto_program.h.
|
inline |
Definition at line 600 of file goto_program.h.
|
inline |
Adds an instruction at the end.
Definition at line 505 of file goto_program.h.
References instructions.
Referenced by disjunctive_polynomial_accelerationt::accelerate(), polynomial_acceleratort::accelerate(), code_contractst::add_contract_check(), string_abstractiont::add_dummy_symbol_and_value(), goto_checkt::add_guarded_claim(), instrumentert::add_instr_to_interleaving(), scratch_programt::append_loop(), scratch_programt::append_path(), disjunctive_polynomial_accelerationt::assert_for_values(), polynomial_acceleratort::assert_for_values(), scratch_programt::assign(), scratch_programt::assume(), sat_path_enumeratort::build_fixed(), disjunctive_polynomial_accelerationt::build_fixed(), build_havoc_code(), havoc_loopst::build_havoc_code(), string_abstractiont::build_new_symbol(), string_abstractiont::build_symbol_constant(), string_abstractiont::char_assign(), check_apply_invariants(), acceleration_utilst::check_inductive(), polynomial_acceleratort::check_inductive(), scratch_programt::check_sat(), dump_ct::cleanup_decl(), static_analysis_baset::concurrent_fixedpoint(), ai_baset::concurrent_fixedpoint(), goto_convertt::convert(), goto_convertt::convert_assert(), goto_convertt::convert_assume(), goto_convertt::convert_break(), goto_convertt::convert_continue(), goto_convertt::convert_CPROVER_throw(), goto_convertt::convert_CPROVER_try_catch(), goto_convertt::convert_dowhile(), goto_convertt::convert_for(), goto_convert_functionst::convert_function(), goto_convertt::convert_gcc_computed_goto(), goto_convertt::convert_goto(), goto_convertt::convert_msc_leave(), goto_convertt::convert_msc_try_finally(), goto_convertt::convert_return(), goto_convertt::convert_skip(), goto_convertt::convert_start_thread(), goto_convertt::convert_switch(), goto_convertt::convert_try_catch(), goto_convertt::convert_while(), goto_convertt::copy(), copy_from(), goto_unwindt::copy_segment(), goto_program_dereferencet::dereference_failure(), acceleration_utilst::do_assumptions(), goto_convertt::do_atomic_begin(), goto_convertt::do_atomic_end(), goto_convertt::do_cpp_new(), string_instrumentationt::do_format_string_read(), string_instrumentationt::do_format_string_write(), string_instrumentationt::do_fscanf(), flow_insensitive_analysis_baset::do_function_call(), goto_convertt::do_function_call_if(), goto_convertt::do_function_call_other(), goto_convertt::do_function_call_symbol(), parameter_assignmentst::do_function_calls(), string_instrumentationt::do_snprintf(), string_instrumentationt::do_sprintf(), string_instrumentationt::do_strchr(), string_instrumentationt::do_strerror(), string_instrumentationt::do_strrchr(), string_instrumentationt::do_strstr(), string_instrumentationt::do_strtok(), acceleration_utilst::ensure_no_overflows(), disjunctive_polynomial_accelerationt::find_path(), polynomial_acceleratort::fit_const(), disjunctive_polynomial_accelerationt::fit_polynomial(), polynomial_acceleratort::fit_polynomial_sliced(), remove_function_pointerst::fix_return_type(), function_exit(), remove_asmt::gcc_asm_function_call(), goto_convertt::generate_conditional_branch(), goto_convertt::generate_ifthenelse(), goto_convertt::generate_thread_block(), goto_checkt::goto_check(), taint_analysist::instrument(), string_instrumentationt::invalidate_buffer(), string_abstractiont::make_decl_and_def(), string_abstractiont::make_val_or_dummy_rec(), sat_path_enumeratort::next(), taint_analysist::operator()(), goto_inlinet::parameter_assignments(), goto_inlinet::parameter_destruction(), remove_asmt::process_instruction(), remove_calls_no_bodyt::remove_call_no_body(), remove_function_pointerst::remove_function_pointer(), goto_convertt::remove_side_effect(), remove_virtual_functionst::remove_virtual_function(), acceleratet::set_dirty_vars(), goto_unwindt::unwind(), string_abstractiont::value_assignments_if(), and string_abstractiont::value_assignments_string_struct().
|
inline |
Adds an instruction of given type at the end.
Definition at line 513 of file goto_program.h.
References instructions.
|
inline |
Clear the goto program.
Definition at line 611 of file goto_program.h.
References instructions.
Referenced by path_acceleratort::clear(), goto_functiont::clear(), copy_from(), goto_program_dereferencet::dereference_program(), goto_checkt::goto_check(), goto_inline(), and string_abstractiont::operator()().
void goto_programt::compute_incoming_edges | ( | ) |
Definition at line 617 of file goto_program.cpp.
References get_successors(), and instructions.
Referenced by copy_from(), and update().
|
inline |
Compute location numbers.
Definition at line 542 of file goto_program.h.
References instructions, and INVARIANT.
Referenced by overflow_instrumentert::add_overflow_checks(), and goto_functionst::compute_location_numbers().
|
inline |
void goto_programt::compute_loop_numbers | ( | ) |
Compute loop numbers.
Definition at line 490 of file goto_program.cpp.
References instructions.
Referenced by update().
void goto_programt::compute_target_numbers | ( | ) |
Compute the target numbers.
Definition at line 519 of file goto_program.cpp.
References DATA_INVARIANT, instructions, and goto_programt::instructiont::nil_target.
Referenced by copy_from(), remove_skip(), and update().
|
inline |
Convert a const_targett to a targett - use with care and avoid whenever possible.
Definition at line 407 of file goto_program.h.
References instructions.
Referenced by goto_unwindt::unwind().
|
inline |
Dummy for templates with possible const contexts.
Definition at line 413 of file goto_program.h.
void goto_programt::copy_from | ( | const goto_programt & | src | ) |
Copy a full goto program, preserving targets.
Definition at line 567 of file goto_program.cpp.
References add_instruction(), clear(), compute_incoming_edges(), compute_target_numbers(), and instructions.
Referenced by scratch_programt::append(), sat_path_enumeratort::build_fixed(), disjunctive_polynomial_accelerationt::build_fixed(), goto_functiont::copy_from(), goto_inlinet::insert_function_body(), instrumentert::is_cfg_spurious(), and path_acceleratort::path_acceleratort().
|
inline |
Appends the given program, which is destroyed.
Definition at line 486 of file goto_program.h.
References instructions.
Referenced by code_contractst::add_contract_check(), scratch_programt::append(), goto_convertt::convert_CPROVER_try_catch(), goto_convertt::convert_dowhile(), goto_convertt::convert_for(), goto_convertt::convert_gcc_switch_case_range(), goto_convertt::convert_label(), goto_convertt::convert_msc_try_finally(), goto_convertt::convert_return(), goto_convertt::convert_switch(), goto_convertt::convert_switch_case(), goto_convertt::convert_try_catch(), goto_convertt::convert_while(), goto_convertt::do_cpp_new(), goto_convertt::do_function_call_if(), goto_convertt::generate_conditional_branch(), goto_convertt::generate_ifthenelse(), goto_convertt::generate_thread_block(), goto_inlinet::insert_function_body(), string_abstractiont::operator()(), taint_analysist::operator()(), remove_asmt::process_instruction(), remove_function_pointerst::remove_function_pointer(), goto_convertt::remove_post(), goto_convertt::remove_statement_expression(), and remove_virtual_functionst::remove_virtual_function().
|
inline |
Inserts the given program at the given location.
The program is destroyed.
Definition at line 495 of file goto_program.h.
References instructions.
Referenced by code_contractst::add_contract_check(), goto_convertt::finish_gotos(), goto_inlinet::insert_function_body(), acceleratet::insert_looping_path(), insert_nondet_init_code(), remove_java_newt::lower_java_new_array(), remove_calls_no_bodyt::remove_call_no_body(), remove_function_pointerst::remove_function_pointer(), remove_virtual_functionst::remove_virtual_function(), and goto_unwindt::unwind().
|
inline |
Is the program empty?
Definition at line 590 of file goto_program.h.
References instructions.
Referenced by goto_inlinet::goto_inline_logt::add_segment(), uncaught_exceptions_analysist::collect_uncaught_exceptions(), goto_convertt::convert_block(), goto_unwindt::copy_segment(), goto_inlinet::expand_function_call(), ai_baset::fixedpoint(), get_function_id(), goto_inlinet::goto_inline_transitive(), dependence_grapht::initialize(), goto_inlinet::insert_function_body(), taint_analysist::instrument(), remove_exceptionst::instrument_exceptions(), goto_inlinet::parameter_assignments(), goto_inlinet::parameter_destruction(), remove_calls_no_bodyt::remove_call_no_body(), remove_virtual_functionst::remove_virtual_function(), and goto_unwindt::unwind().
void goto_programt::get_decl_identifiers | ( | decl_identifierst & | decl_identifiers | ) | const |
get the variables in decl statements
Definition at line 217 of file goto_program.cpp.
References DATA_INVARIANT, forall_goto_program_instructions, and to_symbol_expr().
Referenced by invariant_propagationt::add_objects(), value_set_analysis_fit::add_vars(), value_set_analysis_fivrt::add_vars(), value_set_analysis_fivrnst::add_vars(), and get_local_identifiers().
|
inline |
Definition at line 616 of file goto_program.h.
References DATA_INVARIANT, instructions, and PRECONDITION.
Referenced by remove_exceptionst::find_universal_exception().
|
inline |
Definition at line 625 of file goto_program.h.
References DATA_INVARIANT, instructions, and PRECONDITION.
|
inlinestatic |
Definition at line 418 of file goto_program.h.
Referenced by get_function_id(), and dependence_grapht::initialize().
|
inlinestatic |
Definition at line 427 of file goto_program.h.
References empty(), get_function_id(), instructions, and PRECONDITION.
std::list< Target > goto_programt::get_successors | ( | Target | target | ) | const |
Definition at line 646 of file goto_program.h.
References goto_programt::instructiont::guard, instructions, goto_programt::instructiont::is_assume(), goto_programt::instructiont::is_end_thread(), exprt::is_false(), goto_programt::instructiont::is_goto(), goto_programt::instructiont::is_start_thread(), goto_programt::instructiont::is_throw(), exprt::is_true(), and goto_programt::instructiont::targets.
Referenced by all_paths_enumeratort::backtrack(), trace_automatont::build_alphabet(), sat_path_enumeratort::build_path(), disjunctive_polynomial_accelerationt::build_path(), compute_incoming_edges(), all_paths_enumeratort::extend_path(), sat_path_enumeratort::find_distinguishing_points(), disjunctive_polynomial_accelerationt::find_distinguishing_points(), remove_unreachable(), show_call_sequences(), flow_insensitive_analysis_baset::visit(), static_analysis_baset::visit(), ai_baset::visit(), and dott::write_dot_subgraph().
bool goto_programt::has_assertion | ( | ) | const |
Does the goto program have an assertion?
Definition at line 608 of file goto_program.cpp.
References instructions.
|
inline |
Insertion after the given target.
Definition at line 480 of file goto_program.h.
References instructions.
Referenced by overflow_instrumentert::accumulate_overflow(), uninitializedt::add_assertions(), remove_exceptionst::add_exception_dispatch_sequence(), branch(), sat_path_enumeratort::build_fixed(), disjunctive_polynomial_accelerationt::build_fixed(), remove_returnst::do_function_calls(), goto_convertt::finish_computed_gotos(), remove_exceptionst::instrument_exception_handler(), remove_exceptionst::instrument_function_call(), interrupt(), remove_instanceoft::lower_instanceof(), remove_java_newt::lower_java_new(), acceleratet::make_overflow_loc(), and mutex_init_instrumentation().
|
inline |
Insertion before the given target.
Definition at line 473 of file goto_program.h.
References instructions.
Referenced by w_guardst::add_initialization(), overflow_instrumentert::add_overflow_checks(), shared_bufferst::assignment(), sat_path_enumeratort::build_fixed(), disjunctive_polynomial_accelerationt::build_fixed(), check_and_replace_target(), goto_program2codet::convert_goto_switch(), acceleratet::decl(), shared_bufferst::flush_read(), function_enter(), acceleratet::insert_looping_path(), cover_branch_instrumentert::instrument(), remove_java_newt::lower_java_new_array(), mmio(), race_check(), skip_loops(), stack_depth(), goto_unwindt::unwind(), shared_bufferst::cfg_visitort::weak_memory(), and shared_bufferst::write().
|
inline |
Insertion that preserves jumps to "target".
Definition at line 441 of file goto_program.h.
References instructions, and PRECONDITION.
Referenced by string_abstractiont::abstract_pointer_assign(), acceleratet::accelerate_loop(), uninitializedt::add_assertions(), acceleratet::add_dirty_checks(), code_contractst::apply_contract(), string_abstractiont::char_assign(), goto_program2codet::convert_goto_switch(), cover_instrument_end_of_function(), string_abstractiont::declare_define_locals(), goto_program_dereferencet::dereference_program(), string_instrumentationt::do_fscanf(), parameter_assignmentst::do_function_calls(), string_instrumentationt::do_snprintf(), string_instrumentationt::do_sprintf(), string_instrumentationt::do_strchr(), string_instrumentationt::do_strerror(), string_instrumentationt::do_strrchr(), string_instrumentationt::do_strstr(), string_instrumentationt::do_strtok(), function_exit(), goto_checkt::goto_check(), havoc_loopst::havoc_loop(), acceleratet::insert_automaton(), insert_before_swap(), cover_location_instrumentert::instrument(), cover_branch_instrumentert::instrument(), cover_condition_instrumentert::instrument(), cover_decision_instrumentert::instrument(), cover_mcdc_instrumentert::instrument(), instrument_preconditions(), introduce_temporaries(), k_inductiont::process_loop(), stack_depth(), thread_exit_instrumentation(), string_abstractiont::value_assignments_if(), and string_abstractiont::value_assignments_string_struct().
|
inline |
Insertion that preserves jumps to "target".
The instruction is destroyed.
Definition at line 450 of file goto_program.h.
References insert_before_swap().
|
inline |
Insertion that preserves jumps to "target".
The program p is destroyed.
Definition at line 458 of file goto_program.h.
References insert_before_swap(), instructions, and PRECONDITION.
|
inlinestatic |
Human-readable loop name.
Definition at line 583 of file goto_program.h.
References goto_programt::instructiont::function, id2string(), goto_programt::instructiont::loop_number, and to_string().
Referenced by symex_bmct::get_unwind(), goto_symext::symex_goto(), and goto_symext::symex_transition().
|
delete |
|
inline |
Definition at line 88 of file goto_program.h.
References instructions.
std::ostream & goto_programt::output | ( | const namespacet & | ns, |
const irep_idt & | identifier, | ||
std::ostream & | out | ||
) | const |
Output goto program to given stream.
Definition at line 506 of file goto_program.cpp.
References instructions, and output_instruction().
Referenced by acceleration_utilst::check_inductive(), polynomial_acceleratort::check_inductive(), scratch_programt::check_sat(), acceleration_utilst::do_assumptions(), polynomial_acceleratort::fit_polynomial_sliced(), and output().
|
inline |
Output goto-program to given stream.
Definition at line 526 of file goto_program.h.
References output().
std::ostream & goto_programt::output_instruction | ( | const namespacet & | ns, |
const irep_idt & | identifier, | ||
std::ostream & | out, | ||
const instructionst::value_type & | it | ||
) | const |
Output a single instruction.
Writes to out
a two/three line string representation of a given instruction
.
The output is of the format:
ns | the namespace to resolve the expressions in |
identifier | the identifier used to find a symbol to identify the source language |
out | the stream to write the goto string to |
instruction | the instruction to convert |
Definition at line 34 of file goto_program.cpp.
References source_locationt::as_string(), ASSERT, ASSIGN, ASSUME, ATOMIC_BEGIN, ATOMIC_END, CATCH, goto_programt::instructiont::code, comment(), DATA_INVARIANT, DEAD, DECL, END_FUNCTION, END_THREAD, irept::find(), from_expr(), from_type(), FUNCTION_CALL, source_locationt::get_comment(), codet::get_statement(), irept::get_sub(), goto_programt::instructiont::get_target(), GOTO, goto_programt::instructiont::guard, goto_programt::instructiont::is_assume(), irept::is_nil(), goto_programt::instructiont::is_target(), exprt::is_true(), goto_programt::instructiont::labels, LOCATION, goto_programt::instructiont::location_number, NO_INSTRUCTION_TYPE, exprt::op0(), exprt::operands(), OTHER, RETURN, SKIP, goto_programt::instructiont::source_location, START_THREAD, goto_programt::instructiont::target_number, goto_programt::instructiont::targets, THROW, to_code_landingpad(), goto_programt::instructiont::type, and UNREACHABLE.
Referenced by disjunctive_polynomial_accelerationt::accelerate(), enumerating_loop_accelerationt::accelerate(), polynomial_acceleratort::accelerate(), add_to_json(), goto_instrument_parse_optionst::doit(), goto_inlinet::expand_function_call(), local_bitvector_analysist::output(), local_may_aliast::output(), value_set_analysis_fivrt::output(), value_set_analysis_fivrnst::output(), static_analysis_baset::output(), ai_baset::output(), output(), output_dead_plain(), unified_difft::output_diff(), goto_inlinet::output_inline_map(), change_impactt::output_instruction(), ai_baset::output_json(), output_path(), ai_baset::output_xml(), and goto_unwindt::unwind().
|
inline |
Swap the goto program.
Definition at line 605 of file goto_program.h.
References instructions.
Referenced by goto_convertt::generate_ifthenelse(), string_abstractiont::operator()(), and goto_functiont::swap().
void goto_programt::update | ( | ) |
Update all indices.
Definition at line 498 of file goto_program.cpp.
References compute_incoming_edges(), compute_location_numbers(), compute_loop_numbers(), and compute_target_numbers().
Referenced by acceleratet::accelerate_loop(), acceleratet::accelerate_loops(), scratch_programt::append_loop(), sat_path_enumeratort::build_fixed(), disjunctive_polynomial_accelerationt::build_fixed(), check_and_replace_target(), insert_nondet_init_code(), remove_instanceoft::lower_instanceof(), remove_java_newt::lower_java_new(), race_check(), remove_skip(), remove_unreachable(), remove_virtual_function(), and remove_virtual_functionst::remove_virtual_functions().
|
inline |
Sets the function
member of each instruction if not yet set Note that a goto program need not be a goto function and therefore, we cannot do this in update(), but only at the level of of goto_functionst where goto programs are guaranteed to be named functions.
Definition at line 558 of file goto_program.h.
References instructions.
Referenced by goto_functiont::update_instructions_function().
instructionst goto_programt::instructions |
The list of instructions in the goto program.
Definition at line 403 of file goto_program.h.
Referenced by disjunctive_polynomial_accelerationt::accelerate(), polynomial_acceleratort::accelerate(), acceleratet::accelerate_loop(), code_contractst::add_contract_check(), acceleratet::add_dirty_checks(), w_guardst::add_initialization(), shared_bufferst::add_initialization(), add_instruction(), overflow_instrumentert::add_overflow_checks(), goto_inlinet::goto_inline_logt::add_segment(), add_to_json(), add_to_xml(), value_set_analysis_fit::add_vars(), scratch_programt::append(), scratch_programt::append_loop(), scratch_programt::append_path(), goto_functiont::body_available(), local_cfgt::build(), sat_path_enumeratort::build_fixed(), disjunctive_polynomial_accelerationt::build_fixed(), string_abstractiont::build_new_symbol(), change_impactt::change_impact(), check_and_replace_target(), clear(), compute_called_functions_from_ai(), cfg_baset< cfg_nodet >::compute_edges(), cfg_baset< cfg_nodet >::compute_edges_catch(), cfg_baset< cfg_nodet >::compute_edges_function_call(), procedure_local_cfg_baset< nodet, goto_programt, goto_programt::targett >::compute_edges_function_call(), cfg_baset< cfg_nodet >::compute_edges_goto(), cfg_baset< cfg_nodet >::compute_edges_start_thread(), compute_incoming_edges(), compute_location_numbers(), compute_loop_numbers(), compute_target_numbers(), static_analysis_baset::concurrent_fixedpoint(), ai_baset::concurrent_fixedpoint(), cone_of_influencet::cone_of_influence(), const_cast_target(), goto_convertt::convert(), goto_program2codet::convert_assign_varargs(), goto_convertt::convert_block(), goto_convertt::convert_CPROVER_try_catch(), goto_program2codet::convert_decl(), goto_convertt::convert_dowhile(), goto_convertt::convert_for(), goto_convertt::convert_gcc_switch_case_range(), goto_program2codet::convert_goto(), goto_program2codet::convert_goto_break_continue(), goto_program2codet::convert_goto_if(), goto_program2codet::convert_goto_switch(), goto_program2codet::convert_goto_while(), goto_program2codet::convert_instruction(), goto_convertt::convert_label(), goto_convertt::convert_loop_invariant(), goto_convertt::convert_msc_try_finally(), convert_nondet(), convert_properties_json(), goto_program2codet::convert_return(), goto_program2codet::convert_start_thread(), goto_convertt::convert_switch_case(), goto_convertt::convert_try_catch(), goto_convertt::convert_while(), goto_inlinet::goto_inline_logt::copy_from(), copy_from(), goto_unwindt::copy_segment(), cover_instrument_end_of_function(), string_abstractiont::declare_define_locals(), goto_program_dereferencet::dereference_program(), destructive_append(), destructive_insert(), goto_convertt::do_function_call_if(), parameter_assignmentst::do_function_calls(), empty(), ai_baset::entry_state(), goto_inlinet::expand_function_call(), find_property(), scratch_programt::fix_types(), flow_insensitive_analysis_baset::fixedpoint(), static_analysis_baset::fixedpoint(), ai_baset::fixedpoint(), function_enter(), function_exit(), goto_convertt::generate_ifthenelse(), goto_program2codet::get_cases(), unified_difft::get_diff(), get_end_function(), get_function_id(), get_successors(), cone_of_influencet::get_succs(), goto_checkt::goto_check(), goto_inlinet::goto_inline_transitive(), goto_partial_inline(), has_assertion(), has_start_thread(), invariant_propagationt::initialize(), acceleratet::insert_accelerator(), insert_after(), acceleratet::insert_automaton(), insert_before(), insert_before_swap(), goto_inlinet::insert_function_body(), concurrency_instrumentationt::instrument(), cover_branch_instrumentert::instrument(), instrument_preconditions(), instrumentert::is_cfg_spurious(), is_size_one(), is_skip(), label_properties(), unified_difft::lcss(), list_functions(), remove_instanceoft::lower_instanceof(), remove_java_newt::lower_java_new(), remove_java_newt::lower_java_new_array(), linker_script_merget::ls_data2instructions(), make_assertions_false(), model_argc_argv(), does_remove_constt::operator()(), remove_calls_no_bodyt::operator()(), taint_analysist::operator()(), goto_program2codet::operator()(), operator=(), goto_convertt::optimize_guarded_gotos(), output(), change_impactt::output_change_impact(), output_dead_plain(), goto_difft::output_function(), goto_inlinet::parameter_assignments(), print_path_lengths(), k_inductiont::process_loop(), goto_program2codet::remove_default(), remove_preconditions(), remove_skip(), remove_unreachable(), remove_virtual_functionst::remove_virtual_function(), remove_virtual_functionst::remove_virtual_functions(), replace_java_nondet(), goto_inlinet::replace_return(), cover_basic_blockst::report_block_anomalies(), goto_program2codet::set_block_end_points(), set_properties(), show_call_sequences(), show_locations(), show_properties(), skip_loops(), stack_depth(), swap(), thread_exit_instrumentation(), trace_automatont::trace_automatont(), remove_returnst::undo_function_calls(), unified_difft::unified_diff(), goto_unwindt::unwind(), update_instructions_function(), flow_insensitive_analysis_baset::visit(), static_analysis_baset::visit(), ai_baset::visit(), and dott::write_dot_subgraph().