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:
+ Collaboration diagram for goto_programt:

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
 Get control-flow successors of a given instruction. More...
 
void compute_incoming_edges ()
 Compute for each instruction the set of instructions it is a successor of. More...
 
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 instruction pointed-to by the given instruction iterator target. More...
 
targett insert_after (const_targett target)
 Insertion after the instruction pointed-to by the given instruction iterator target. More...
 
void destructive_append (goto_programt &p)
 Appends the given program p to *this. p is destroyed. More...
 
void destructive_insert (const_targett target, goto_programt &p)
 Inserts the given program p before target. 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 &instruction) 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 ()
 Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program. More...
 
const_targett get_end_function () const
 Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program. More...
 
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...
 
bool equals (const goto_programt &other) const
 Syntactic equality: two goto_programt are equal if, and only if, they have the same number of instructions, each pair of instructions compares equal, and relative jumps have the same distance. More...
 
void validate (const namespacet &ns, const validation_modet vm) const
 Check that the goto program is well-formed. More...
 

Static Public Member Functions

static const irep_idt get_function_id (const_targett l)
 Get the id of the function that contains the instruction pointed-to by the given instruction iterator. More...
 
static const irep_idt get_function_id (const goto_programt &p)
 Get the id of the function that contains the given goto program. More...
 
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 72 of file goto_program.h.

Member Typedef Documentation

◆ const_targetst

Definition at line 417 of file goto_program.h.

◆ const_targett

typedef instructionst::const_iterator goto_programt::const_targett

Definition at line 415 of file goto_program.h.

◆ decl_identifierst

Definition at line 680 of file goto_program.h.

◆ instructionst

Definition at line 412 of file goto_program.h.

◆ targetst

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

Definition at line 416 of file goto_program.h.

◆ targett

typedef instructionst::iterator goto_programt::targett

Definition at line 414 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 85 of file goto_program.h.

◆ goto_programt() [3/3]

goto_programt::goto_programt ( )
inline

Constructor.

Definition at line 632 of file goto_program.h.

◆ ~goto_programt()

goto_programt::~goto_programt ( )
inline

Definition at line 636 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 541 of file goto_program.h.

◆ 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 549 of file goto_program.h.

◆ clear()

void goto_programt::clear ( void  )
inline

Clear the goto program.

Definition at line 647 of file goto_program.h.

◆ compute_incoming_edges()

void goto_programt::compute_incoming_edges ( )

Compute for each instruction the set of instructions it is a successor of.

Definition at line 640 of file goto_program.cpp.

◆ compute_location_numbers() [1/2]

void goto_programt::compute_location_numbers ( unsigned &  nr)
inline

Compute location numbers.

Definition at line 578 of file goto_program.h.

◆ compute_location_numbers() [2/2]

void goto_programt::compute_location_numbers ( )
inline

Compute location numbers.

Definition at line 606 of file goto_program.h.

◆ compute_loop_numbers()

void goto_programt::compute_loop_numbers ( )

Compute loop numbers.

Assign each loop in the goto program a unique index.

Every backwards goto is considered a loop. The loops are numbered starting from zero and in the order they appear in the goto program.

Definition at line 496 of file goto_program.cpp.

◆ compute_target_numbers()

void goto_programt::compute_target_numbers ( )

Compute the target numbers.

Assign each target (i.e., an instruction that is in the targets list of another instruction) a unique index.

Instructions that are not targets get target number instructiont::nil_target. The targets are numbered starting from one and in the order they appear in the goto program. An instruction is considered a target if it is the target of a control-flow instruction (either GOTO or START_THREAD), i.e., it is contained in the targets list of those instructions. Instructions that are reached via straight-line control flow (fall-through for GOTO instructions) only are not considered targets.

Definition at line 535 of file goto_program.cpp.

◆ 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 424 of file goto_program.h.

◆ 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 430 of file goto_program.h.

◆ copy_from()

void goto_programt::copy_from ( const goto_programt src)

Copy a full goto program, preserving targets.

Copy other goto program into this goto program.

The current goto program is cleared, and targets are adjusted as needed

Parameters
srcthe goto program to copy from

Definition at line 589 of file goto_program.cpp.

◆ destructive_append()

void goto_programt::destructive_append ( goto_programt p)
inline

Appends the given program p to *this. p is destroyed.

Definition at line 524 of file goto_program.h.

◆ destructive_insert()

void goto_programt::destructive_insert ( const_targett  target,
goto_programt p 
)
inline

Inserts the given program p before target.

The program p is destroyed.

Definition at line 532 of file goto_program.h.

◆ empty()

bool goto_programt::empty ( ) const
inline

Is the program empty?

Definition at line 626 of file goto_program.h.

◆ equals()

bool goto_programt::equals ( const goto_programt other) const

Syntactic equality: two goto_programt are equal if, and only if, they have the same number of instructions, each pair of instructions compares equal, and relative jumps have the same distance.

Definition at line 728 of file goto_program.cpp.

◆ get_decl_identifiers()

void goto_programt::get_decl_identifiers ( decl_identifierst decl_identifiers) const

get the variables in decl statements

Definition at line 220 of file goto_program.cpp.

◆ get_end_function() [1/2]

targett goto_programt::get_end_function ( )
inline

Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program.

Definition at line 654 of file goto_program.h.

◆ get_end_function() [2/2]

const_targett goto_programt::get_end_function ( ) const
inline

Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program.

Definition at line 665 of file goto_program.h.

◆ get_function_id() [1/2]

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

Get the id of the function that contains the instruction pointed-to by the given instruction iterator.

Parameters
linstruction iterator
Returns
id of the function that contains the pointed-to goto instruction

Definition at line 440 of file goto_program.h.

◆ get_function_id() [2/2]

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

Get the id of the function that contains the given goto program.

Parameters
pthe goto program
Returns
id of the function that contains the goto program

Definition at line 463 of file goto_program.h.

◆ get_successors()

template<typename Target >
std::list< Target > goto_programt::get_successors ( Target  target) const

Get control-flow successors of a given instruction.

The instruction is represented by a pointer target of type Target. An instruction has either 0, 1, or 2 successors (more than two successors is deprecated). For example, an ASSUME instruction with the guard being a false_exprt has 0 successors, and ASSIGN instruction has 1 successor, and a GOTO instruction with the guard not being a true_exprt has 2 successors.

Template Parameters
Targettype used to represent a pointer to an instruction in a goto program
Parameters
targetpointer to the instruction of which to get the successors of
Returns
List of control-flow successors of the pointed-to goto program instruction

Definition at line 715 of file goto_program.h.

◆ has_assertion()

bool goto_programt::has_assertion ( ) const

Does the goto program have an assertion?

Returns true if the goto program includes an ASSERT instruction the guard of which is not trivially true.

Definition at line 630 of file goto_program.cpp.

◆ insert_after()

targett goto_programt::insert_after ( const_targett  target)
inline

Insertion after the instruction pointed-to by the given instruction iterator target.

Returns
newly inserted location

Definition at line 518 of file goto_program.h.

◆ insert_before()

targett goto_programt::insert_before ( const_targett  target)
inline

Insertion before the instruction pointed-to by the given instruction iterator target.

Returns
newly inserted location

Definition at line 510 of file goto_program.h.

◆ insert_before_swap() [1/3]

void goto_programt::insert_before_swap ( targett  target)
inline

Insertion that preserves jumps to "target".

Definition at line 477 of file goto_program.h.

◆ 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 486 of file goto_program.h.

◆ 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 494 of file goto_program.h.

◆ loop_id()

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

Human-readable loop name.

Definition at line 619 of file goto_program.h.

◆ 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 90 of file goto_program.h.

◆ output() [1/2]

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

Output goto program to given stream.

Definition at line 512 of file goto_program.cpp.

◆ output() [2/2]

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

Output goto-program to given stream.

Definition at line 562 of file goto_program.h.

◆ output_instruction()

std::ostream & goto_programt::output_instruction ( const namespacet ns,
const irep_idt identifier,
std::ostream &  out,
const instructionst::value_type &  instruction 
) 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 35 of file goto_program.cpp.

◆ swap()

void goto_programt::swap ( goto_programt program)
inline

Swap the goto program.

Definition at line 641 of file goto_program.h.

◆ update()

void goto_programt::update ( )

Update all indices.

Definition at line 504 of file goto_program.cpp.

◆ 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 594 of file goto_program.h.

◆ validate()

void goto_programt::validate ( const namespacet ns,
const validation_modet  vm 
) const
inline

Check that the goto program is well-formed.

The validation mode indicates whether well-formedness check failures are reported via DATA_INVARIANT violations or exceptions.

Definition at line 693 of file goto_program.h.

Member Data Documentation

◆ instructions

instructionst goto_programt::instructions

The list of instructions in the goto program.

Definition at line 420 of file goto_program.h.


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