ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
goto_programt Class Reference
Goto programs

A generic container class for a control flow graph for one function, in the form of a goto-program. More...

#include <goto_program.h>

Classes

class  instructiont
 Container for an instruction of the goto-program. More...

Public Types

typedef std::list< class instructiont > instructionst
typedef instructionst::iterator targett
typedef instructionst::const_iterator const_targett
typedef std::list< targett > targetst
typedef std::list< const_targett > const_targetst
typedef std::set< irep_idt > decl_identifierst

Public Member Functions

 goto_programt (const goto_programt &src)
 copy constructor
goto_programt & operator= (const goto_programt &src)
 assignment operator
void get_successors (const_targett target, const_targetst &successors) const
void insert_swap (targett target)
 Insertion that preserves jumps to "target".
void insert_swap (targett target, instructiont &instruction)
void insert_swap (targett target, goto_programt &p)
targett insert (targett target)
void destructive_append (goto_programt &p)
 Appends the given program, which is destroyed.
void destructive_insert (targett target, goto_programt &p)
targett add_instruction ()
targett add_instruction (instructiont &instruction)
targett add_instruction (goto_program_instruction_typet type)
void dump () const
 Output goto program to given stream.
std::ostream & output (const namespacet &ns, const irep_idt &identifier, std::ostream &out) const
 Output goto-program to given stream.
void update_instructions_function (const irep_idt &function_id, bool force=false)
 Sets the function member of each instruction if not yet set, or unconditionally when force is true (e.g.
void compute_target_numbers ()
 Compute the target numbers.
void compute_location_numbers (unsigned &nr)
 Compute location numbers.
void compute_location_numbers ()
 Compute location numbers.
void compute_loop_numbers (unsigned int &num)
 Compute loop numbers.
void update ()
 Update all indices.
bool empty () const
 Is the program empty?
 goto_programt ()
 Constructor.
virtual ~goto_programt ()=default
void swap (goto_programt &program)
 Swap the goto program.
void clear ()
 Clear the goto program.
void copy_from (const goto_programt &src)
 Copy a full goto program, preserving targets.
void get_decl_identifiers (decl_identifierst &decl_identifiers) const
 get the variables in decl statements

Public Attributes

bool hide
instructionst instructions
 The list of instructions in the goto program.

Detailed Description

A generic container class for a control flow graph for one function, in the form of a goto-program.

Member Typedef Documentation

◆ const_targetst

typedef std::list<const_targett> goto_programt::const_targetst

◆ const_targett

typedef instructionst::const_iterator goto_programt::const_targett

◆ decl_identifierst

typedef std::set<irep_idt> goto_programt::decl_identifierst

◆ instructionst

typedef std::list<class instructiont> goto_programt::instructionst

◆ targetst

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

◆ targett

typedef instructionst::iterator goto_programt::targett

Constructor & Destructor Documentation

◆ goto_programt() [1/2]

goto_programt::goto_programt ( const goto_programt & src)
inline

copy constructor

Parameters
[in]srcthe goto program to copy from

◆ goto_programt() [2/2]

goto_programt::goto_programt ( )
inline

Constructor.

◆ ~goto_programt()

virtual goto_programt::~goto_programt ( )
virtualdefault

Member Function Documentation

◆ add_instruction() [1/3]

targett goto_programt::add_instruction ( )
inline

Adds an instruction at the end.

Returns
The newly added instruction.

◆ add_instruction() [2/3]

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.

◆ add_instruction() [3/3]

targett goto_programt::add_instruction ( instructiont & instruction)
inline

Adds a copy of the given instruction at the end.

Returns
The newly added instruction.

◆ clear()

void goto_programt::clear ( )
inline

Clear the goto program.

◆ compute_location_numbers() [1/2]

void goto_programt::compute_location_numbers ( )
inline

Compute location numbers.

◆ compute_location_numbers() [2/2]

void goto_programt::compute_location_numbers ( unsigned & nr)
inline

Compute location numbers.

◆ compute_loop_numbers()

void goto_programt::compute_loop_numbers ( unsigned int & num)

Compute loop numbers.

◆ compute_target_numbers()

void goto_programt::compute_target_numbers ( )

Compute the target numbers.

◆ copy_from()

void goto_programt::copy_from ( const goto_programt & src)

Copy a full goto program, preserving targets.

◆ destructive_append()

void goto_programt::destructive_append ( goto_programt & p)
inline

Appends the given program, which is destroyed.

◆ destructive_insert()

void goto_programt::destructive_insert ( targett target,
goto_programt & p )
inline

Inserts the given program at the given location. The program is destroyed.

◆ dump()

void goto_programt::dump ( ) const

Output goto program to given stream.

◆ empty()

bool goto_programt::empty ( ) const
inline

Is the program empty?

◆ get_decl_identifiers()

void goto_programt::get_decl_identifiers ( decl_identifierst & decl_identifiers) const

get the variables in decl statements

◆ get_successors()

void goto_programt::get_successors ( const_targett target,
const_targetst & successors ) const

◆ insert()

targett goto_programt::insert ( targett target)
inline

Insertion before the given target

Returns
newly inserted location

◆ insert_swap() [1/3]

void goto_programt::insert_swap ( targett target)
inline

Insertion that preserves jumps to "target".

◆ insert_swap() [2/3]

void goto_programt::insert_swap ( targett target,
goto_programt & p )
inline

Insertion that preserves jumps to "target". The program p is destroyed.

◆ insert_swap() [3/3]

void goto_programt::insert_swap ( targett target,
instructiont & instruction )
inline

Insertion that preserves jumps to "target". The instruction is destroyed.

◆ operator=()

goto_programt & goto_programt::operator= ( const goto_programt & src)
inline

assignment operator

Parameters
[in]srcthe goto program to copy from

◆ output()

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

Output goto-program to given stream.

◆ swap()

void goto_programt::swap ( goto_programt & program)
inline

Swap the goto program.

◆ update()

void goto_programt::update ( )

Update all indices.

◆ update_instructions_function()

void goto_programt::update_instructions_function ( const irep_idt & function_id,
bool force = false )
inline

Sets the function member of each instruction if not yet set, or unconditionally when force is true (e.g.

to re-tag a body copied from another function, as contract renaming does). 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.

Member Data Documentation

◆ hide

bool goto_programt::hide

◆ instructions

instructionst goto_programt::instructions

The list of instructions in the goto program.

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