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.

◆ 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

◆ 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

◆ 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: