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< 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 instructiont::target_less_than	target_less_than

typedef std::set< irep_idt >	decl_identifierst

Public Member Functions
	goto_programt (const goto_programt &)=delete
	Copying is deleted as this class contains pointers that cannot be copied. More...

goto_programt &	operator= (const goto_programt &)=delete

	goto_programt (goto_programt &&other)

goto_programt &	operator= (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 (std::ostream &out) const
	Output goto-program to given stream. 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_set_return_value (exprt return_value, const source_locationt &l=source_locationt::nil())

static instructiont	make_set_return_value (const code_returnt &code, const source_locationt &l=source_locationt::nil())=delete

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 goto_instruction_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 source_locationt &l=source_locationt::nil())

static instructiont	make_incomplete_goto (const code_gotot &, const source_locationt &=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 lhs, 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

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

Definition at line 617 of file goto_program.h.

◆ const_targett

typedef instructionst::const_iterator goto_programt::const_targett

Definition at line 615 of file goto_program.h.

◆ decl_identifierst

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

Definition at line 853 of file goto_program.h.

◆ instructionst

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

Definition at line 612 of file goto_program.h.

◆ target_less_than

typedef instructiont::target_less_than goto_programt::target_less_than

Definition at line 619 of file goto_program.h.

◆ targetst

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

Definition at line 616 of file goto_program.h.

◆ targett

typedef instructionst::iterator goto_programt::targett

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

◆ ~goto_programt()

goto_programt::~goto_programt ( )

inline

Definition at line 809 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 739 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 747 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 754 of file goto_program.h.

◆ clear()

void goto_programt::clear ( void )

inline

Clear the goto program.

Definition at line 820 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 752 of file goto_program.cpp.

◆ compute_location_numbers() [1/2]

void goto_programt::compute_location_numbers ( )

inline

Compute location numbers.

Definition at line 778 of file goto_program.h.

◆ compute_location_numbers() [2/2]

void goto_programt::compute_location_numbers ( unsigned & nr )

inline

Compute location numbers.

Definition at line 766 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 611 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 647 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 626 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 632 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

src	the goto program to copy from

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

◆ empty()

bool goto_programt::empty ( ) const

inline

Is the program empty?

Definition at line 799 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 1140 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 319 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 827 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 838 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

Target type used to represent a pointer to an instruction in a goto program

Parameters

target pointer 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 1126 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 742 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 708 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 716 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 692 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 700 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 643 of file goto_program.h.

◆ insert_before_swap() [2/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 676 of file goto_program.h.

◆ insert_before_swap() [3/3]

void goto_programt::insert_before_swap	(	targett	target,
		instructiont &	instruction
	)

inline

Insertion that preserves jumps to "target".

The instruction is destroyed.

Turns:

...->[a]->...
      ^
    target

Into:

...->[i]->[a]->...
      ^
    target

So that jumps to a now jump to the newly inserted i.

Definition at line 668 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 792 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 933 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 1065 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 1073 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 945 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 979 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 990 of file goto_program.h.

◆ make_catch()

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

inlinestatic

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

◆ make_decl() [1/2]

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

inlinestatic

Definition at line 1082 of file goto_program.h.

◆ make_decl() [2/2]

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

inlinestatic

Definition at line 964 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 1001 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 1090 of file goto_program.h.

◆ make_function_call() [2/2]

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

inlinestatic

Create a function call instruction.

Definition at line 1098 of file goto_program.h.

◆ make_goto() [1/2]

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

inlinestatic

Definition at line 1051 of file goto_program.h.

◆ make_goto() [2/2]

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

inlinestatic

Definition at line 1039 of file goto_program.h.

◆ make_incomplete_goto() [1/3]

goto_programt::instructiont goto_programt::make_incomplete_goto	(	const code_gotot &	_code,
		const source_locationt &	l = `source_locationt::nil()`
	)

static

Definition at line 33 of file goto_program.cpp.

◆ make_incomplete_goto() [2/3]

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

inlinestatic

Definition at line 1011 of file goto_program.h.

◆ make_incomplete_goto() [3/3]

static instructiont goto_programt::make_incomplete_goto ( const source_locationt & l = source_locationt::nil() )

inlinestatic

Definition at line 1025 of file goto_program.h.

◆ make_location()

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

inlinestatic

Definition at line 901 of file goto_program.h.

◆ make_other()

static instructiont goto_programt::make_other	(	const goto_instruction_codet &	_code,
		const source_locationt &	l = `source_locationt::nil()`
	)

inlinestatic

Definition at line 957 of file goto_program.h.

◆ make_set_return_value() [1/2]

static instructiont goto_programt::make_set_return_value	(	const code_returnt &	code,
		const source_locationt &	l = `source_locationt::nil()`
	)

staticdelete

◆ make_set_return_value() [2/2]

static instructiont goto_programt::make_set_return_value	(	exprt	return_value,
		const source_locationt &	l = `source_locationt::nil()`
	)

inlinestatic

Definition at line 874 of file goto_program.h.

◆ make_skip()

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

inlinestatic

Definition at line 891 of file goto_program.h.

◆ make_throw()

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

inlinestatic

Definition at line 912 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()

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

Output goto-program to given stream.

Definition at line 627 of file goto_program.cpp.

◆ swap()

void goto_programt::swap ( goto_programt & program )

inline

Swap the goto program.

Definition at line 814 of file goto_program.h.

◆ update()

void goto_programt::update ( )

Update all indices.

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

Member Data Documentation

◆ instructions

instructionst goto_programt::instructions

The list of instructions in the goto program.

Definition at line 622 of file goto_program.h.

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

/home/runner/work/cbmc/cbmc/src/goto-programs/goto_program.h
/home/runner/work/cbmc/cbmc/src/goto-programs/goto_program.cpp

Classes

Public Types

Public Member Functions

Static Public Member Functions

Public Attributes

Detailed Description

Member Typedef Documentation

◆ const_targetst

◆ const_targett

◆ decl_identifierst

◆ instructionst

◆ target_less_than

◆ targetst

◆ targett

Constructor & Destructor Documentation

◆ goto_programt() [1/3]

◆ goto_programt() [2/3]

◆ goto_programt() [3/3]

◆ ~goto_programt()

Member Function Documentation

◆ add()

◆ add_instruction() [1/2]

◆ add_instruction() [2/2]

◆ clear()

◆ compute_incoming_edges()

◆ compute_location_numbers() [1/2]

◆ compute_location_numbers() [2/2]

◆ compute_loop_numbers()

◆ compute_target_numbers()

◆ const_cast_target() [1/2]

◆ const_cast_target() [2/2]

◆ copy_from()

◆ destructive_append()

◆ destructive_insert()

◆ empty()

◆ equals()

◆ get_decl_identifiers()

◆ get_end_function() [1/2]

◆ get_end_function() [2/2]

◆ get_successors()

◆ has_assertion()

◆ insert_after() [1/2]

◆ insert_after() [2/2]

◆ insert_before() [1/2]

◆ insert_before() [2/2]

◆ insert_before_swap() [1/3]

◆ insert_before_swap() [2/3]

◆ insert_before_swap() [3/3]

◆ loop_id()

◆ make_assertion()

◆ make_assignment() [1/2]

◆ make_assignment() [2/2]

◆ make_assumption()

◆ make_atomic_begin()

◆ make_atomic_end()

◆ make_catch()

◆ make_dead()

◆ make_decl() [1/2]

◆ make_decl() [2/2]

◆ make_end_function()

◆ make_function_call() [1/2]

◆ make_function_call() [2/2]

◆ make_goto() [1/2]

◆ make_goto() [2/2]

◆ make_incomplete_goto() [1/3]

◆ make_incomplete_goto() [2/3]

◆ make_incomplete_goto() [3/3]

◆ make_location()

◆ make_other()

◆ make_set_return_value() [1/2]

◆ make_set_return_value() [2/2]

◆ make_skip()

◆ make_throw()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ output()

◆ swap()

◆ update()

◆ validate()

Member Data Documentation