cprover
goto_program_templatet< codeT, guardT > Class Template Referenceabstract

A generic container class for the GOTO intermediate representation of one function. More...

#include <goto_program_template.h>

Inheritance diagram for goto_program_templatet< codeT, guardT >:
[legend]
Collaboration diagram for goto_program_templatet< codeT, guardT >:
[legend]

Classes

class  instructiont
 This class represents an instruction in the GOTO intermediate representation. More...
 

Public Types

typedef std::list< instructiontinstructionst
 
typedef instructionst::iterator targett
 
typedef instructionst::const_iterator const_targett
 
typedef std::list< targetttargetst
 
typedef std::list< const_targettconst_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_templatetoperator= (const goto_program_templatet &)=delete
 
 goto_program_templatet (goto_program_templatet &&other)
 
goto_program_templatetoperator= (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...
 

Detailed Description

template<class codeT, class guardT>
class goto_program_templatet< codeT, guardT >

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.

Member Typedef Documentation

◆ const_targetst

template<class codeT, class guardT>
typedef std::list<const_targett> goto_program_templatet< codeT, guardT >::const_targetst

Definition at line 349 of file goto_program_template.h.

◆ const_targett

template<class codeT, class guardT>
typedef instructionst::const_iterator goto_program_templatet< codeT, guardT >::const_targett

Definition at line 347 of file goto_program_template.h.

◆ instructionst

template<class codeT, class guardT>
typedef std::list<instructiont> goto_program_templatet< codeT, guardT >::instructionst

Definition at line 344 of file goto_program_template.h.

◆ targetst

template<class codeT, class guardT>
typedef std::list<targett> goto_program_templatet< codeT, guardT >::targetst

Definition at line 348 of file goto_program_template.h.

◆ targett

template<class codeT, class guardT>
typedef instructionst::iterator goto_program_templatet< codeT, guardT >::targett

Definition at line 346 of file goto_program_template.h.

Constructor & Destructor Documentation

◆ goto_program_templatet() [1/3]

template<class codeT, class guardT>
goto_program_templatet< codeT, guardT >::goto_program_templatet ( const goto_program_templatet< codeT, guardT > &  )
delete

Copying is deleted as this class contains pointers that cannot be copied.

◆ goto_program_templatet() [2/3]

template<class codeT, class guardT>
goto_program_templatet< codeT, guardT >::goto_program_templatet ( goto_program_templatet< codeT, guardT > &&  other)
inline

Definition at line 82 of file goto_program_template.h.

◆ goto_program_templatet() [3/3]

template<class codeT, class guardT>
goto_program_templatet< codeT, guardT >::goto_program_templatet ( )
inline

Constructor.

Definition at line 524 of file goto_program_template.h.

◆ ~goto_program_templatet()

template<class codeT, class guardT>
virtual goto_program_templatet< codeT, guardT >::~goto_program_templatet ( )
inlinevirtual

Definition at line 528 of file goto_program_template.h.

Member Function Documentation

◆ add_instruction() [1/2]

template<class codeT, class guardT>
targett goto_program_templatet< codeT, guardT >::add_instruction ( )
inline

Adds an instruction at the end.

Returns
The newly added instruction.

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

◆ add_instruction() [2/2]

template<class codeT, class guardT>
targett goto_program_templatet< codeT, guardT >::add_instruction ( goto_program_instruction_typet  type)
inline

Adds an instruction of given type at the end.

Returns
The newly added instruction.

Definition at line 462 of file goto_program_template.h.

◆ clear()

template<class codeT, class guardT>
void goto_program_templatet< codeT, guardT >::clear ( void  )
inline

◆ compute_incoming_edges()

template<class codeT , class guardT >
void goto_program_templatet< codeT, guardT >::compute_incoming_edges ( )

Definition at line 757 of file goto_program_template.h.

Referenced by remove_skip().

◆ compute_location_numbers() [1/2]

template<class codeT, class guardT>
void goto_program_templatet< codeT, guardT >::compute_location_numbers ( unsigned &  nr)
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().

◆ compute_location_numbers() [2/2]

template<class codeT, class guardT>
void goto_program_templatet< codeT, guardT >::compute_location_numbers ( )
inline

Compute location numbers.

Definition at line 498 of file goto_program_template.h.

Referenced by goto_program_templatet< codet, exprt >::compute_location_numbers().

◆ compute_loop_numbers()

template<class codeT , class guardT >
void goto_program_templatet< codeT, guardT >::compute_loop_numbers ( )

Compute loop numbers.

Definition at line 560 of file goto_program_template.h.

◆ compute_target_numbers()

template<class codeT , class guardT >
void goto_program_templatet< codeT, guardT >::compute_target_numbers ( )

Compute the target numbers.

Definition at line 657 of file goto_program_template.h.

◆ const_cast_target() [1/2]

template<class codeT, class guardT>
targett goto_program_templatet< codeT, guardT >::const_cast_target ( const_targett  t)
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().

◆ const_cast_target() [2/2]

template<class codeT, class guardT>
const_targett goto_program_templatet< codeT, guardT >::const_cast_target ( const_targett  t) const
inline

Dummy for templates with possible const contexts.

Definition at line 362 of file goto_program_template.h.

◆ copy_from()

template<class codeT, class guardT>
void goto_program_templatet< codeT, guardT >::copy_from ( const goto_program_templatet< codeT, guardT > &  src)

◆ destructive_append()

◆ destructive_insert()

template<class codeT, class guardT>
void goto_program_templatet< codeT, guardT >::destructive_insert ( const_targett  target,
goto_program_templatet< codeT, guardT > &  p 
)
inline

◆ empty()

◆ get_end_function()

template<class codeT, class guardT>
targett goto_program_templatet< codeT, guardT >::get_end_function ( )
inline

◆ get_function_id() [1/2]

template<class codeT, class guardT>
static const irep_idt goto_program_templatet< codeT, guardT >::get_function_id ( const_targett  l)
inlinestatic

◆ get_function_id() [2/2]

template<class codeT, class guardT>
static const irep_idt goto_program_templatet< codeT, guardT >::get_function_id ( const goto_program_templatet< codeT, guardT > &  p)
inlinestatic

Definition at line 376 of file goto_program_template.h.

◆ get_successors()

◆ has_assertion()

template<class codeT , class guardT >
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.

◆ insert_after()

◆ insert_before()

◆ insert_before_swap() [1/3]

◆ insert_before_swap() [2/3]

template<class codeT, class guardT>
void goto_program_templatet< codeT, guardT >::insert_before_swap ( targett  target,
instructiont instruction 
)
inline

Insertion that preserves jumps to "target".

The instruction is destroyed.

Definition at line 399 of file goto_program_template.h.

◆ insert_before_swap() [3/3]

template<class codeT, class guardT>
void goto_program_templatet< codeT, guardT >::insert_before_swap ( targett  target,
goto_program_templatet< codeT, guardT > &  p 
)
inline

Insertion that preserves jumps to "target".

The program p is destroyed.

Definition at line 407 of file goto_program_template.h.

◆ loop_id()

template<class codeT, class guardT>
static irep_idt goto_program_templatet< codeT, guardT >::loop_id ( const_targett  target)
inlinestatic

Human-readable loop name.

Definition at line 511 of file goto_program_template.h.

◆ operator=() [1/2]

template<class codeT, class guardT>
goto_program_templatet& goto_program_templatet< codeT, guardT >::operator= ( const goto_program_templatet< codeT, guardT > &  )
delete

◆ operator=() [2/2]

template<class codeT, class guardT>
goto_program_templatet& goto_program_templatet< codeT, guardT >::operator= ( goto_program_templatet< codeT, guardT > &&  other)
inline

Definition at line 87 of file goto_program_template.h.

◆ output() [1/2]

template<class codeT , class guardT >
std::ostream & goto_program_templatet< codeT, guardT >::output ( const namespacet ns,
const irep_idt identifier,
std::ostream &  out 
) const

◆ output() [2/2]

template<class codeT, class guardT>
std::ostream& goto_program_templatet< codeT, guardT >::output ( std::ostream &  out) const
inline

Output goto-program to given stream.

Definition at line 475 of file goto_program_template.h.

◆ output_instruction()

template<class codeT, class guardT>
virtual std::ostream& goto_program_templatet< codeT, guardT >::output_instruction ( const namespacet ns,
const irep_idt identifier,
std::ostream &  out,
typename instructionst::const_iterator  it 
) const
pure virtual

Output a single instruction.

◆ swap()

template<class codeT, class guardT>
void goto_program_templatet< codeT, guardT >::swap ( goto_program_templatet< codeT, guardT > &  program)
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()().

◆ update()

Member Data Documentation

◆ instructions

template<class codeT, class guardT>
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().


The documentation for this class was generated from the following file: