cprover
goto_programt Class Reference

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

#include <goto_program.h>

Inheritance diagram for goto_programt:
[legend]
Collaboration diagram for goto_programt:
[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
 
typedef std::set< irep_idtdecl_identifierst
 

Public Member Functions

 goto_programt (const goto_programt &)=delete
 Copying is deleted as this class contains pointers that cannot be copied. More...
 
goto_programtoperator= (const goto_programt &)=delete
 
 goto_programt (goto_programt &&other)
 
goto_programtoperator= (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...
 

Detailed Description

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.

Member Typedef Documentation

◆ const_targetst

Definition at line 400 of file goto_program.h.

◆ const_targett

typedef instructionst::const_iterator goto_programt::const_targett

Definition at line 398 of file goto_program.h.

◆ decl_identifierst

Definition at line 640 of file goto_program.h.

◆ instructionst

Definition at line 395 of file goto_program.h.

◆ targetst

typedef std::list<targett> goto_programt::targetst

Definition at line 399 of file goto_program.h.

◆ targett

typedef instructionst::iterator goto_programt::targett

Definition at line 397 of file goto_program.h.

Constructor & Destructor Documentation

◆ goto_programt() [1/3]

goto_programt::goto_programt ( const goto_programt )
delete

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

◆ goto_programt() [2/3]

goto_programt::goto_programt ( goto_programt &&  other)
inline

Definition at line 83 of file goto_program.h.

◆ goto_programt() [3/3]

goto_programt::goto_programt ( )
inline

Constructor.

Definition at line 596 of file goto_program.h.

◆ ~goto_programt()

goto_programt::~goto_programt ( )
inline

Definition at line 600 of file goto_program.h.

Member Function Documentation

◆ add_instruction() [1/2]

targett goto_programt::add_instruction ( )
inline

Adds an instruction at the end.

Returns
The newly added instruction.

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(), remove_asmt::msc_asm_function_call(), sat_path_enumeratort::next(), taint_analysist::operator()(), goto_inlinet::parameter_assignments(), goto_inlinet::parameter_destruction(), remove_asmt::process_instruction_gcc(), remove_asmt::process_instruction_msc(), 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().

◆ add_instruction() [2/2]

targett goto_programt::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 513 of file goto_program.h.

References instructions.

◆ clear()

void goto_programt::clear ( void  )
inline

◆ compute_incoming_edges()

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

◆ compute_location_numbers() [1/2]

void goto_programt::compute_location_numbers ( unsigned &  nr)
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().

◆ compute_location_numbers() [2/2]

void goto_programt::compute_location_numbers ( )
inline

Compute location numbers.

Definition at line 570 of file goto_program.h.

Referenced by update().

◆ compute_loop_numbers()

void goto_programt::compute_loop_numbers ( )

Compute loop numbers.

Definition at line 490 of file goto_program.cpp.

References instructions.

Referenced by update().

◆ compute_target_numbers()

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

◆ const_cast_target() [1/2]

targett goto_programt::const_cast_target ( const_targett  t)
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().

◆ const_cast_target() [2/2]

const_targett goto_programt::const_cast_target ( const_targett  t) const
inline

Dummy for templates with possible const contexts.

Definition at line 413 of file goto_program.h.

◆ copy_from()

◆ destructive_append()

◆ destructive_insert()

◆ empty()

◆ get_decl_identifiers()

void goto_programt::get_decl_identifiers ( decl_identifierst decl_identifiers) const

◆ get_end_function() [1/2]

targett goto_programt::get_end_function ( )
inline

Definition at line 616 of file goto_program.h.

References DATA_INVARIANT, instructions, and PRECONDITION.

Referenced by remove_exceptionst::find_universal_exception().

◆ get_end_function() [2/2]

const_targett goto_programt::get_end_function ( ) const
inline

Definition at line 625 of file goto_program.h.

References DATA_INVARIANT, instructions, and PRECONDITION.

◆ get_function_id() [1/2]

static const irep_idt goto_programt::get_function_id ( const_targett  l)
inlinestatic

◆ get_function_id() [2/2]

static const irep_idt goto_programt::get_function_id ( const goto_programt p)
inlinestatic

Definition at line 427 of file goto_program.h.

References empty(), get_function_id(), instructions, and PRECONDITION.

◆ get_successors()

◆ has_assertion()

bool goto_programt::has_assertion ( ) const

Does the goto program have an assertion?

Definition at line 608 of file goto_program.cpp.

References instructions.

◆ insert_after()

◆ insert_before()

◆ insert_before_swap() [1/3]

void goto_programt::insert_before_swap ( targett  target)
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(), insert_nondet_init_code(), cover_location_instrumentert::instrument(), cover_branch_instrumentert::instrument(), cover_condition_instrumentert::instrument(), cover_decision_instrumentert::instrument(), cover_mcdc_instrumentert::instrument(), instrument_preconditions(), introduce_temporaries(), remove_instanceoft::lower_instanceof(), k_inductiont::process_loop(), stack_depth(), thread_exit_instrumentation(), string_abstractiont::value_assignments_if(), and string_abstractiont::value_assignments_string_struct().

◆ insert_before_swap() [2/3]

void goto_programt::insert_before_swap ( targett  target,
instructiont instruction 
)
inline

Insertion that preserves jumps to "target".

The instruction is destroyed.

Definition at line 450 of file goto_program.h.

References insert_before_swap().

◆ insert_before_swap() [3/3]

void goto_programt::insert_before_swap ( targett  target,
goto_programt p 
)
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.

◆ loop_id()

static irep_idt goto_programt::loop_id ( const instructiont instruction)
inlinestatic

◆ operator=() [1/2]

goto_programt& goto_programt::operator= ( const goto_programt )
delete

◆ operator=() [2/2]

goto_programt& goto_programt::operator= ( goto_programt &&  other)
inline

Definition at line 88 of file goto_program.h.

References instructions.

◆ output() [1/2]

std::ostream & goto_programt::output ( const namespacet ns,
const irep_idt identifier,
std::ostream &  out 
) const

◆ output() [2/2]

std::ostream& goto_programt::output ( std::ostream &  out) const
inline

Output goto-program to given stream.

Definition at line 526 of file goto_program.h.

References output().

◆ output_instruction()

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:

// {location} file {source file} line {line in source file}
// Labels: {list-of-labels}
{representation of the instruction}
Parameters
nsthe namespace to resolve the expressions in
identifierthe identifier used to find a symbol to identify the source language
outthe stream to write the goto string to
instructionthe instruction to convert
Returns
Appends to out a two line representation of the instruction

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(), local_safe_pointerst::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(), local_safe_pointerst::output_safe_dereferences(), ai_baset::output_xml(), and goto_unwindt::unwind().

◆ swap()

void goto_programt::swap ( goto_programt program)
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().

◆ update()

◆ update_instructions_function()

void goto_programt::update_instructions_function ( const irep_idt function_id)
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().

Member Data Documentation

◆ instructions

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()(), replace_callst::operator()(), remove_calls_no_bodyt::operator()(), taint_analysist::operator()(), local_safe_pointerst::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().


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