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 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 (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_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 589 of file goto_program.h.

◆ const_targett

typedef instructionst::const_iterator goto_programt::const_targett

Definition at line 587 of file goto_program.h.

◆ decl_identifierst

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

Definition at line 844 of file goto_program.h.

◆ instructionst

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

Definition at line 584 of file goto_program.h.

◆ targetst

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

Definition at line 588 of file goto_program.h.

◆ targett

typedef instructionst::iterator goto_programt::targett

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

◆ ~goto_programt()

goto_programt::~goto_programt ( )

inline

Definition at line 800 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 709 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 717 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 724 of file goto_program.h.

◆ clear()

void goto_programt::clear ( )

inline

Clear the goto program.

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

◆ compute_location_numbers() [1/2]

void goto_programt::compute_location_numbers ( )

inline

Compute location numbers.

Definition at line 769 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 757 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 609 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 645 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 596 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 602 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 699 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 692 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 700 of file goto_program.h.

◆ empty()

bool goto_programt::empty ( ) const

inline

Is the program empty?

Definition at line 790 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 1138 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 317 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 818 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 829 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 1117 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 740 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 678 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 686 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 662 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 670 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 613 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 646 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 638 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 783 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 924 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 1056 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 1064 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 936 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 970 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 981 of file goto_program.h.

◆ make_catch()

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

inlinestatic

Definition at line 914 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 962 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 1073 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 955 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 992 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 1081 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 1089 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 1042 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 1030 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 31 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 1002 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 1016 of file goto_program.h.

◆ make_location()

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

inlinestatic

Definition at line 892 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 948 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 865 of file goto_program.h.

◆ make_skip()

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

inlinestatic

Definition at line 882 of file goto_program.h.

◆ make_throw()

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

inlinestatic

Definition at line 903 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

inline

Output goto program to given stream.

Deprecated:: "deprecated since " "2022" "-" "5" "-" "29" "; " "Use output(out) instead"

Definition at line 731 of file goto_program.h.

◆ output() [2/2]

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

Output goto-program to given stream.

Definition at line 625 of file goto_program.cpp.

◆ output_instruction()

std::ostream& goto_programt::output_instruction	(	const namespacet &	ns,
		const irep_idt &	identifier,
		std::ostream &	out,
		const instructionst::value_type &	instruction
	)		const

inline

Output a single instruction.

Deprecated:: "deprecated since " "2022" "-" "5" "-" "29" "; " "Use instruction.output(out) instead"

Definition at line 744 of file goto_program.h.

◆ swap()

void goto_programt::swap ( goto_programt & program )

inline

Swap the goto program.

Definition at line 805 of file goto_program.h.

◆ update()

void goto_programt::update ( )

Update all indices.

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

Member Data Documentation

◆ instructions

instructionst goto_programt::instructions

The list of instructions in the goto program.

Definition at line 592 of file goto_program.h.

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

/home/runner/work/cbmc-documentation/cbmc-documentation/src/goto-programs/goto_program.h
/home/runner/work/cbmc-documentation/cbmc-documentation/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

◆ 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() [1/2]

◆ output() [2/2]

◆ output_instruction()

◆ swap()

◆ update()

◆ validate()