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_before (const_targett target, const instructiont &i)
 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...
 
targett insert_after (const_targett target, const instructiont &i)
 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 (instructiont &&instruction)
 Adds a given instruction at the end. 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 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 irep_idt loop_id (const irep_idt &function_id, const instructiont &instruction)
 Human-readable loop name. More...
 
static instructiont make_return (const source_locationt &l=source_locationt::nil())
 
static instructiont make_return (code_returnt c, const source_locationt &l=source_locationt::nil())
 
static instructiont make_skip (const source_locationt &l=source_locationt::nil())
 
static instructiont make_location (const source_locationt &l)
 
static instructiont make_throw (const source_locationt &l=source_locationt::nil())
 
static instructiont make_catch (const source_locationt &l=source_locationt::nil())
 
static instructiont make_assertion (const exprt &g, const source_locationt &l=source_locationt::nil())
 
static instructiont make_assumption (const exprt &g, const source_locationt &l=source_locationt::nil())
 
static instructiont make_other (const codet &_code, const source_locationt &l=source_locationt::nil())
 
static instructiont make_decl (const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
 
static instructiont make_dead (const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
 
static instructiont make_atomic_begin (const source_locationt &l=source_locationt::nil())
 
static instructiont make_atomic_end (const source_locationt &l=source_locationt::nil())
 
static instructiont make_end_function (const source_locationt &l=source_locationt::nil())
 
static instructiont make_incomplete_goto (const exprt &_cond, const source_locationt &l=source_locationt::nil())
 
static instructiont make_incomplete_goto (const code_gotot &_code, const source_locationt &l=source_locationt::nil())
 
static instructiont make_goto (targett _target, const source_locationt &l=source_locationt::nil())
 
static instructiont make_goto (targett _target, const exprt &g, const source_locationt &l=source_locationt::nil())
 
static instructiont make_assignment (const code_assignt &_code, const source_locationt &l=source_locationt::nil())
 Create an assignment instruction. More...
 
static instructiont make_assignment (exprt lhs, exprt rhs, const source_locationt &l=source_locationt::nil())
 Create an assignment instruction. More...
 
static instructiont make_decl (const code_declt &_code, const source_locationt &l=source_locationt::nil())
 
static instructiont make_function_call (const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
 Create a function call instruction. More...
 
static instructiont make_function_call (exprt function, code_function_callt::argumentst arguments, const source_locationt &l=source_locationt::nil())
 Create a function call instruction. 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 582 of file goto_program.h.

◆ const_targett

typedef instructionst::const_iterator goto_programt::const_targett

Definition at line 580 of file goto_program.h.

◆ decl_identifierst

Definition at line 816 of file goto_program.h.

◆ instructionst

Definition at line 577 of file goto_program.h.

◆ targetst

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

Definition at line 581 of file goto_program.h.

◆ targett

typedef instructionst::iterator goto_programt::targett

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

◆ ~goto_programt()

goto_programt::~goto_programt ( )
inline

Definition at line 772 of file goto_program.h.

Member Function Documentation

◆ add()

targett goto_programt::add ( instructiont &&  instruction)
inline

Adds a given instruction at the end.

Returns
The newly added instruction.

Definition at line 686 of file goto_program.h.

◆ add_instruction() [1/2]

targett goto_programt::add_instruction ( )
inline

Adds an instruction at the end.

Returns
The newly added instruction.

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

◆ clear()

void goto_programt::clear ( void  )
inline

Clear the goto program.

Definition at line 783 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 673 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 729 of file goto_program.h.

◆ compute_location_numbers() [2/2]

void goto_programt::compute_location_numbers ( )
inline

Compute location numbers.

Definition at line 741 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 529 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 568 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 589 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 595 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 622 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 669 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 677 of file goto_program.h.

◆ empty()

bool goto_programt::empty ( ) const
inline

Is the program empty?

Definition at line 762 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 1079 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 225 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 790 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 801 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 1073 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 663 of file goto_program.cpp.

◆ insert_after() [1/2]

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

◆ insert_after() [2/2]

targett goto_programt::insert_after ( const_targett  target,
const instructiont i 
)
inline

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

Returns
newly inserted location

Definition at line 663 of file goto_program.h.

◆ insert_before() [1/2]

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

◆ insert_before() [2/2]

targett goto_programt::insert_before ( const_targett  target,
const instructiont i 
)
inline

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

Returns
newly inserted location

Definition at line 647 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 606 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 615 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 623 of file goto_program.h.

◆ loop_id()

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

Human-readable loop name.

Definition at line 755 of file goto_program.h.

◆ make_assertion()

static instructiont goto_programt::make_assertion ( const exprt g,
const source_locationt l = source_locationt::nil() 
)
inlinestatic

Definition at line 893 of file goto_program.h.

◆ make_assignment() [1/2]

static instructiont goto_programt::make_assignment ( const code_assignt _code,
const source_locationt l = source_locationt::nil() 
)
inlinestatic

Create an assignment instruction.

Definition at line 1013 of file goto_program.h.

◆ make_assignment() [2/2]

static instructiont goto_programt::make_assignment ( exprt  lhs,
exprt  rhs,
const source_locationt l = source_locationt::nil() 
)
inlinestatic

Create an assignment instruction.

Definition at line 1021 of file goto_program.h.

◆ make_assumption()

static instructiont goto_programt::make_assumption ( const exprt g,
const source_locationt l = source_locationt::nil() 
)
inlinestatic

Definition at line 905 of file goto_program.h.

◆ make_atomic_begin()

static instructiont goto_programt::make_atomic_begin ( const source_locationt l = source_locationt::nil())
inlinestatic

Definition at line 935 of file goto_program.h.

◆ make_atomic_end()

static instructiont goto_programt::make_atomic_end ( const source_locationt l = source_locationt::nil())
inlinestatic

Definition at line 946 of file goto_program.h.

◆ make_catch()

static instructiont goto_programt::make_catch ( const source_locationt l = source_locationt::nil())
inlinestatic

Definition at line 883 of file goto_program.h.

◆ make_dead()

static instructiont goto_programt::make_dead ( const symbol_exprt symbol,
const source_locationt l = source_locationt::nil() 
)
inlinestatic

Definition at line 927 of file goto_program.h.

◆ make_decl() [1/2]

static instructiont goto_programt::make_decl ( const symbol_exprt symbol,
const source_locationt l = source_locationt::nil() 
)
inlinestatic

Definition at line 920 of file goto_program.h.

◆ make_decl() [2/2]

static instructiont goto_programt::make_decl ( const code_declt _code,
const source_locationt l = source_locationt::nil() 
)
inlinestatic

Definition at line 1030 of file goto_program.h.

◆ make_end_function()

static instructiont goto_programt::make_end_function ( const source_locationt l = source_locationt::nil())
inlinestatic

Definition at line 957 of file goto_program.h.

◆ make_function_call() [1/2]

static instructiont goto_programt::make_function_call ( const code_function_callt _code,
const source_locationt l = source_locationt::nil() 
)
inlinestatic

Create a function call instruction.

Definition at line 1038 of file goto_program.h.

◆ make_function_call() [2/2]

static instructiont goto_programt::make_function_call ( exprt  function,
code_function_callt::argumentst  arguments,
const source_locationt l = source_locationt::nil() 
)
inlinestatic

Create a function call instruction.

Definition at line 1046 of file goto_program.h.

◆ make_goto() [1/2]

static instructiont goto_programt::make_goto ( targett  _target,
const source_locationt l = source_locationt::nil() 
)
inlinestatic

Definition at line 987 of file goto_program.h.

◆ make_goto() [2/2]

static instructiont goto_programt::make_goto ( targett  _target,
const exprt g,
const source_locationt l = source_locationt::nil() 
)
inlinestatic

Definition at line 999 of file goto_program.h.

◆ make_incomplete_goto() [1/2]

static instructiont goto_programt::make_incomplete_goto ( const exprt _cond,
const source_locationt l = source_locationt::nil() 
)
inlinestatic

Definition at line 967 of file goto_program.h.

◆ make_incomplete_goto() [2/2]

static instructiont goto_programt::make_incomplete_goto ( const code_gotot _code,
const source_locationt l = source_locationt::nil() 
)
inlinestatic

Definition at line 980 of file goto_program.h.

◆ make_location()

static instructiont goto_programt::make_location ( const source_locationt l)
inlinestatic

Definition at line 861 of file goto_program.h.

◆ make_other()

static instructiont goto_programt::make_other ( const codet _code,
const source_locationt l = source_locationt::nil() 
)
inlinestatic

Definition at line 913 of file goto_program.h.

◆ make_return() [1/2]

static instructiont goto_programt::make_return ( const source_locationt l = source_locationt::nil())
inlinestatic

Definition at line 838 of file goto_program.h.

◆ make_return() [2/2]

static instructiont goto_programt::make_return ( code_returnt  c,
const source_locationt l = source_locationt::nil() 
)
inlinestatic

Definition at line 843 of file goto_program.h.

◆ make_skip()

static instructiont goto_programt::make_skip ( const source_locationt l = source_locationt::nil())
inlinestatic

Definition at line 851 of file goto_program.h.

◆ make_throw()

static instructiont goto_programt::make_throw ( const source_locationt l = source_locationt::nil())
inlinestatic

Definition at line 872 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 545 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 713 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 41 of file goto_program.cpp.

◆ swap()

void goto_programt::swap ( goto_programt program)
inline

Swap the goto program.

Definition at line 777 of file goto_program.h.

◆ update()

void goto_programt::update ( )

Update all indices.

Definition at line 537 of file goto_program.cpp.

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

Member Data Documentation

◆ instructions

instructionst goto_programt::instructions

The list of instructions in the goto program.

Definition at line 585 of file goto_program.h.


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