cprover
|
A generic container class for the GOTO intermediate representation of one function. More...
#include <goto_program_template.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 |
Public Member Functions | |
goto_program_templatet (const goto_program_templatet &)=delete | |
Copying is deleted as this class contains pointers that cannot be copied. More... | |
goto_program_templatet & | operator= (const goto_program_templatet &)=delete |
goto_program_templatet (goto_program_templatet &&other) | |
goto_program_templatet & | operator= (goto_program_templatet &&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_program_templatet< codeT, guardT > &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_program_templatet< codeT, guardT > &p) |
Appends the given program, which is destroyed. More... | |
void | destructive_insert (const_targett target, goto_program_templatet< codeT, guardT > &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... | |
virtual std::ostream & | output_instruction (const namespacet &ns, const irep_idt &identifier, std::ostream &out, typename instructionst::const_iterator it) const =0 |
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 | 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_program_templatet () | |
Constructor. More... | |
virtual | ~goto_program_templatet () |
void | swap (goto_program_templatet< codeT, guardT > &program) |
Swap the goto program. More... | |
void | clear () |
Clear the goto program. More... | |
targett | get_end_function () |
void | copy_from (const goto_program_templatet< codeT, guardT > &src) |
Copy a full goto program, preserving targets. More... | |
bool | has_assertion () const |
Does the goto program have an assertion? More... | |
Static Public Member Functions | |
static const irep_idt | get_function_id (const_targett l) |
static const irep_idt | get_function_id (const goto_program_templatet< codeT, guardT > &p) |
static irep_idt | loop_id (const_targett target) |
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 69 of file goto_program_template.h.
typedef std::list<const_targett> goto_program_templatet< codeT, guardT >::const_targetst |
Definition at line 349 of file goto_program_template.h.
typedef instructionst::const_iterator goto_program_templatet< codeT, guardT >::const_targett |
Definition at line 347 of file goto_program_template.h.
typedef std::list<instructiont> goto_program_templatet< codeT, guardT >::instructionst |
Definition at line 344 of file goto_program_template.h.
typedef std::list<targett> goto_program_templatet< codeT, guardT >::targetst |
Definition at line 348 of file goto_program_template.h.
typedef instructionst::iterator goto_program_templatet< codeT, guardT >::targett |
Definition at line 346 of file goto_program_template.h.
|
delete |
Copying is deleted as this class contains pointers that cannot be copied.
|
inline |
Definition at line 82 of file goto_program_template.h.
|
inline |
Constructor.
Definition at line 524 of file goto_program_template.h.
|
inlinevirtual |
Definition at line 528 of file goto_program_template.h.
|
inline |
Adds an instruction at the end.
Definition at line 454 of file goto_program_template.h.
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(), disjunctive_polynomial_accelerationt::assert_for_values(), polynomial_acceleratort::assert_for_values(), 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(), dump_ct::cleanup_decl(), static_analysis_baset::concurrent_fixedpoint(), ai_baset::concurrent_fixedpoint(), convert(), xml_goto_program_convertt::convert(), goto_convertt::convert(), goto_convertt::convert_assert(), goto_convertt::convert_assume(), goto_convertt::convert_bp_abortif(), goto_convertt::convert_bp_enforce(), 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_java_try_catch(), goto_convertt::convert_msc_leave(), goto_convertt::convert_msc_try_finally(), goto_convertt::convert_return(), goto_convertt::convert_skip(), goto_convertt::convert_specc_notify(), goto_convertt::convert_specc_wait(), goto_convertt::convert_start_thread(), goto_convertt::convert_switch(), goto_convertt::convert_try_catch(), goto_convertt::convert_while(), goto_convertt::copy(), 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(), goto_convertt::do_java_new(), goto_convertt::do_java_new_array(), 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_checkt::goto_check(), goto_inlinet::insert_function_nobody(), 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_function_pointerst::remove_function_pointer(), goto_convertt::remove_side_effect(), remove_virtual_functionst::remove_virtual_function(), goto_inlinet::replace_return(), 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 462 of file goto_program_template.h.
|
inline |
Clear the goto program.
Definition at line 539 of file goto_program_template.h.
Referenced by path_acceleratort::clear(), convert(), xml_goto_program_convertt::convert(), goto_program_dereferencet::dereference_program(), goto_checkt::goto_check(), and string_abstractiont::operator()().
void goto_program_templatet< codeT, guardT >::compute_incoming_edges | ( | ) |
Definition at line 757 of file goto_program_template.h.
Referenced by remove_skip().
|
inline |
Compute location numbers.
Definition at line 491 of file goto_program_template.h.
Referenced by overflow_instrumentert::add_overflow_checks(), convert(), and xml_goto_program_convertt::convert().
|
inline |
Compute location numbers.
Definition at line 498 of file goto_program_template.h.
Referenced by goto_program_templatet< codet, exprt >::compute_location_numbers().
void goto_program_templatet< codeT, guardT >::compute_loop_numbers | ( | ) |
Compute loop numbers.
Definition at line 560 of file goto_program_template.h.
void goto_program_templatet< codeT, guardT >::compute_target_numbers | ( | ) |
Compute the target numbers.
Definition at line 657 of file goto_program_template.h.
|
inline |
Convert a const_targett to a targett - use with care and avoid whenever possible.
Definition at line 356 of file goto_program_template.h.
Referenced by goto_unwindt::unwind().
|
inline |
Dummy for templates with possible const contexts.
Definition at line 362 of file goto_program_template.h.
void goto_program_templatet< codeT, guardT >::copy_from | ( | const goto_program_templatet< codeT, guardT > & | src | ) |
Copy a full goto program, preserving targets.
Definition at line 704 of file goto_program_template.h.
Referenced by scratch_programt::append(), sat_path_enumeratort::build_fixed(), disjunctive_polynomial_accelerationt::build_fixed(), 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 435 of file goto_program_template.h.
Referenced by code_contractst::add_contract_check(), goto_convertt::convert_bp_enforce(), goto_convertt::convert_CPROVER_try_catch(), goto_convertt::convert_dowhile(), goto_convertt::convert_for(), goto_convertt::convert_gcc_switch_case_range(), goto_convertt::convert_java_try_catch(), goto_convertt::convert_label(), goto_convertt::convert_msc_try_finally(), goto_convertt::convert_return(), goto_convertt::convert_start_thread(), 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::do_java_new_array(), goto_convertt::generate_conditional_branch(), goto_convertt::generate_ifthenelse(), 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 444 of file goto_program_template.h.
Referenced by code_contractst::add_contract_check(), goto_convertt::finish_gotos(), goto_inlinet::insert_function_body(), goto_inlinet::insert_function_nobody(), acceleratet::insert_looping_path(), remove_function_pointerst::remove_function_pointer(), remove_virtual_functionst::remove_virtual_function(), and goto_unwindt::unwind().
|
inline |
Is the program empty?
Definition at line 518 of file goto_program_template.h.
Referenced by remove_exceptionst::add_exceptional_returns(), goto_inlinet::goto_inline_logt::add_segment(), goto_convertt::convert_block(), goto_unwindt::copy_segment(), goto_inlinet::expand_function_call(), ai_baset::fixedpoint(), goto_program_templatet< codet, exprt >::get_function_id(), dependence_grapht::initialize(), goto_inlinet::insert_function_body(), goto_inlinet::insert_function_nobody(), taint_analysist::instrument(), remove_exceptionst::instrument_exceptions(), goto_inlinet::parameter_assignments(), goto_inlinet::parameter_destruction(), remove_returnst::replace_returns(), and goto_unwindt::unwind().
|
inline |
Definition at line 544 of file goto_program_template.h.
Referenced by remove_exceptionst::instrument_function_call(), and remove_exceptionst::instrument_throw().
|
inlinestatic |
Definition at line 367 of file goto_program_template.h.
Referenced by goto_program_templatet< codet, exprt >::get_function_id().
|
inlinestatic |
Definition at line 376 of file goto_program_template.h.
std::list< Target > goto_program_templatet< codeT, guardT >::get_successors | ( | Target | target | ) | const |
Definition at line 570 of file goto_program_template.h.
Referenced by all_paths_enumeratort::backtrack(), trace_automatont::build_alphabet(), sat_path_enumeratort::build_path(), disjunctive_polynomial_accelerationt::build_path(), 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_program_templatet< codeT, guardT >::has_assertion | ( | ) | const |
Does the goto program have an assertion?
Definition at line 747 of file goto_program_template.h.
|
inline |
Insertion after the given target.
Definition at line 429 of file goto_program_template.h.
Referenced by overflow_instrumentert::accumulate_overflow(), uninitializedt::add_assertions(), 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(), remove_exceptionst::instrument_throw(), remove_instanceoft::lower_instanceof(), acceleratet::make_overflow_loc(), mutex_init_instrumentation(), and replace_async().
|
inline |
Insertion before the given target.
Definition at line 422 of file goto_program_template.h.
Referenced by remove_exceptionst::add_exceptional_returns(), w_guardst::add_initialization(), overflow_instrumentert::add_overflow_checks(), shared_bufferst::assignment(), sat_path_enumeratort::build_fixed(), disjunctive_polynomial_accelerationt::build_fixed(), goto_program2codet::convert_goto_switch(), acceleratet::decl(), shared_bufferst::flush_read(), function_enter(), acceleratet::insert_looping_path(), instrument_cover_goals(), 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 390 of file goto_program_template.h.
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(), 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(), acceleratet::insert_automaton(), goto_program_templatet< codet, exprt >::insert_before_swap(), instrument_cover_goals(), introduce_temporaries(), goto_inlinet::replace_return(), 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 399 of file goto_program_template.h.
|
inline |
Insertion that preserves jumps to "target".
The program p is destroyed.
Definition at line 407 of file goto_program_template.h.
|
inlinestatic |
Human-readable loop name.
Definition at line 511 of file goto_program_template.h.
|
delete |
Referenced by goto_programt::operator=().
|
inline |
Definition at line 87 of file goto_program_template.h.
std::ostream & goto_program_templatet< codeT, guardT >::output | ( | const namespacet & | ns, |
const irep_idt & | identifier, | ||
std::ostream & | out | ||
) | const |
Output goto program to given stream.
Definition at line 640 of file goto_program_template.h.
Referenced by acceleration_utilst::check_inductive(), polynomial_acceleratort::check_inductive(), acceleration_utilst::do_assumptions(), polynomial_acceleratort::fit_polynomial_sliced(), and goto_program_templatet< codet, exprt >::output().
|
inline |
Output goto-program to given stream.
Definition at line 475 of file goto_program_template.h.
|
pure virtual |
Output a single instruction.
|
inline |
Swap the goto program.
Definition at line 533 of file goto_program_template.h.
Referenced by goto_convertt::generate_ifthenelse(), and string_abstractiont::operator()().
void goto_program_templatet< codeT, guardT >::update | ( | ) |
Update all indices.
Definition at line 632 of file goto_program_template.h.
Referenced by acceleratet::accelerate_loop(), acceleratet::accelerate_loops(), sat_path_enumeratort::build_fixed(), disjunctive_polynomial_accelerationt::build_fixed(), convert(), xml_goto_program_convertt::convert(), string_instrumentationt::do_function_call(), remove_instanceoft::lower_instanceof(), remove_function_pointerst::remove_function_pointers(), and remove_virtual_functionst::remove_virtual_functions().
instructionst goto_program_templatet< codeT, guardT >::instructions |
The list of instructions in the goto program.
Definition at line 352 of file goto_program_template.h.
Referenced by disjunctive_polynomial_accelerationt::accelerate(), polynomial_acceleratort::accelerate(), acceleratet::accelerate_loop(), code_contractst::add_contract_check(), acceleratet::add_dirty_checks(), remove_exceptionst::add_exceptional_returns(), w_guardst::add_initialization(), shared_bufferst::add_initialization(), goto_program_templatet< codet, exprt >::add_instruction(), overflow_instrumentert::add_overflow_checks(), goto_inlinet::goto_inline_logt::add_segment(), add_to_json(), value_set_analysis_fit::add_vars(), basic_blocks(), local_cfgt::build(), sat_path_enumeratort::build_fixed(), disjunctive_polynomial_accelerationt::build_fixed(), string_abstractiont::build_new_symbol(), change_impactt::change_impact(), goto_program_templatet< codet, exprt >::clear(), 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(), concurrent_cfg_baset< T, P, I >::compute_edges_start_thread(), goto_program_templatet< codet, exprt >::compute_location_numbers(), static_analysis_baset::concurrent_fixedpoint(), ai_baset::concurrent_fixedpoint(), cone_of_influencet::cone_of_influence(), goto_program_templatet< codet, exprt >::const_cast_target(), convert(), xml_goto_program_convertt::convert(), 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_difft::convert_function(), 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(), goto_program2codet::convert_return(), goto_program2codet::convert_start_thread(), goto_convertt::convert_start_thread(), goto_convertt::convert_switch_case(), goto_convertt::convert_try_catch(), goto_convertt::convert_while(), goto_inlinet::goto_inline_logt::copy_from(), goto_program_templatet< codet, exprt >::copy_from(), goto_unwindt::copy_segment(), string_abstractiont::declare_define_locals(), goto_program_dereferencet::dereference_program(), goto_program_templatet< codet, exprt >::destructive_append(), goto_program_templatet< codet, exprt >::destructive_insert(), goto_convertt::do_function_call_if(), parameter_assignmentst::do_function_calls(), goto_program_templatet< codet, exprt >::empty(), ai_baset::entry_state(), 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(), goto_program_templatet< codet, exprt >::get_end_function(), goto_program_templatet< codet, exprt >::get_function_id(), cone_of_influencet::get_succs(), goto_checkt::goto_check(), goto_inlinet::goto_inline_transitive(), goto_partial_inline(), has_start_thread(), invariant_propagationt::initialize(), goto_symex_statet::initialize(), acceleratet::insert_accelerator(), goto_program_templatet< codet, exprt >::insert_after(), acceleratet::insert_automaton(), goto_program_templatet< codet, exprt >::insert_before(), goto_program_templatet< codet, exprt >::insert_before_swap(), goto_inlinet::insert_function_body(), concurrency_instrumentationt::instrument(), instrument_cover_goals(), instrumentert::is_cfg_spurious(), is_size_one(), label_properties(), unified_difft::lcss(), list_functions(), make_assertions_false(), does_remove_constt::operator()(), taint_analysist::operator()(), goto_program2codet::operator()(), goto_symext::operator()(), goto_program_templatet< codet, exprt >::operator=(), output_dead_plain(), goto_difft::output_functions(), goto_inlinet::parameter_assignments(), print_path_lengths(), goto_program2codet::remove_default(), remove_skip(), remove_unreachable(), goto_inlinet::replace_return(), remove_returnst::restore_returns(), goto_program2codet::set_block_end_points(), set_properties(), show_call_sequences(), show_locations(), show_properties(), show_properties_json(), skip_loops(), stack_depth(), goto_program_templatet< codet, exprt >::swap(), thread_exit_instrumentation(), trace_automatont::trace_automatont(), remove_returnst::undo_function_calls(), unified_difft::unified_diff(), goto_unwindt::unwind(), flow_insensitive_analysis_baset::visit(), static_analysis_baset::visit(), ai_baset::visit(), and dott::write_dot_subgraph().