cprover
goto_programt Class Reference

A specialization of goto_program_templatet over goto programs in which instructions have codet type. More...

#include <goto_program.h>

Inheritance diagram for goto_programt:
[legend]
Collaboration diagram for goto_programt:
[legend]

Public Types

typedef std::set< irep_idtdecl_identifierst
 
- Public Types inherited from goto_program_templatet< codet, exprt >
typedef std::list< instructiont > instructionst
 
typedef instructionst::iterator targett
 
typedef instructionst::const_iterator const_targett
 
typedef std::list< targetttargetst
 
typedef std::list< const_targettconst_targetst
 

Public Member Functions

std::ostream & output_instruction (const class namespacet &ns, const irep_idt &identifier, std::ostream &out, instructionst::const_iterator it) const
 See below. More...
 
std::ostream & output_instruction (const class namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructiont &instruction) const
 
 goto_programt ()
 
 goto_programt (const goto_programt &)=delete
 
goto_programtoperator= (const goto_programt &)=delete
 
 goto_programt (goto_programt &&other)
 
goto_programtoperator= (goto_programt &&other)
 
void get_decl_identifiers (decl_identifierst &decl_identifiers) const
 
- Public Member Functions inherited from goto_program_templatet< codet, exprt >
 goto_program_templatet (const goto_program_templatet &)=delete
 Copying is deleted as this class contains pointers that cannot be copied. More...
 
 goto_program_templatet (goto_program_templatet &&other)
 
 goto_program_templatet ()
 Constructor. More...
 
goto_program_templatetoperator= (const goto_program_templatet &)=delete
 
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...
 
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, exprt > &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, exprt > &p)
 Appends the given program, which is destroyed. More...
 
void destructive_insert (const_targett target, goto_program_templatet< codet, exprt > &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...
 
virtual ~goto_program_templatet ()
 
void swap (goto_program_templatet< codet, exprt > &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, exprt > &src)
 Copy a full goto program, preserving targets. More...
 
bool has_assertion () const
 Does the goto program have an assertion? More...
 

Additional Inherited Members

- Static Public Member Functions inherited from goto_program_templatet< codet, exprt >
static const irep_idt get_function_id (const_targett l)
 
static const irep_idt get_function_id (const goto_program_templatet< codet, exprt > &p)
 
static irep_idt loop_id (const_targett target)
 Human-readable loop name. More...
 
- Public Attributes inherited from goto_program_templatet< codet, exprt >
instructionst instructions
 The list of instructions in the goto program. More...
 

Detailed Description

A specialization of goto_program_templatet over goto programs in which instructions have codet type.

Definition at line 24 of file goto_program.h.

Member Typedef Documentation

§ decl_identifierst

Definition at line 64 of file goto_program.h.

Constructor & Destructor Documentation

§ goto_programt() [1/3]

goto_programt::goto_programt ( )
inline

Definition at line 39 of file goto_program.h.

References operator=().

§ goto_programt() [2/3]

goto_programt::goto_programt ( const goto_programt )
delete

§ goto_programt() [3/3]

goto_programt::goto_programt ( goto_programt &&  other)
inline

Definition at line 52 of file goto_program.h.

Member Function Documentation

§ get_decl_identifiers()

§ operator=() [1/2]

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

Referenced by goto_programt().

§ operator=() [2/2]

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

§ output_instruction() [1/2]

std::ostream & goto_programt::output_instruction ( const class namespacet ns,
const irep_idt identifier,
std::ostream &  out,
instructionst::const_iterator  it 
) const

See below.

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
itan iterator pointing to the instruction to convert
Returns
See below.

Definition at line 27 of file goto_program.cpp.

References source_locationt::as_string(), ASSERT, ASSIGN, ASSUME, ATOMIC_BEGIN, ATOMIC_END, CATCH, goto_program_templatet< codeT, guardT >::instructiont::code, comment(), DEAD, DECL, END_FUNCTION, END_THREAD, from_expr(), FUNCTION_CALL, source_locationt::get_comment(), GOTO, goto_program_templatet< codeT, guardT >::instructiont::guard, goto_program_templatet< codeT, guardT >::instructiont::is_assume(), irept::is_nil(), goto_program_templatet< codeT, guardT >::instructiont::is_target(), goto_program_templatet< codeT, guardT >::instructiont::labels, LOCATION, goto_program_templatet< codeT, guardT >::instructiont::location_number, NO_INSTRUCTION_TYPE, OTHER, RETURN, SKIP, goto_program_templatet< codeT, guardT >::instructiont::source_location, START_THREAD, goto_program_templatet< codeT, guardT >::instructiont::target_number, goto_program_templatet< codeT, guardT >::instructiont::targets, THROW, and goto_program_templatet< codeT, guardT >::instructiont::type.

Referenced by enumerating_loop_accelerationt::accelerate(), disjunctive_polynomial_accelerationt::accelerate(), polynomial_acceleratort::accelerate(), add_to_json(), goto_instrument_parse_optionst::doit(), goto_inlinet::expand_function_call(), value_set_analysis_fivrt::output(), value_set_analysis_fivrnst::output(), static_analysis_baset::output(), ai_baset::output(), output_dead_plain(), unified_difft::output_diff(), change_impactt::output_instruction(), ai_baset::output_json(), output_path(), ai_baset::output_xml(), and goto_unwindt::unwind().

§ output_instruction() [2/2]

std::ostream& goto_programt::output_instruction ( const class namespacet ns,
const irep_idt identifier,
std::ostream &  out,
const instructiont &  instruction 
) const

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