This class represents an instruction in the GOTO intermediate representation. More...

#include <goto_program.h>

Collaboration diagram for goto_programt::instructiont:

Public Types
typedef std::list< instructiont >::iterator	targett
	The target for gotos and for start_thread nodes. More...

typedef std::list< instructiont >::const_iterator	const_targett

typedef std::list< targett >	targetst

typedef std::list< const_targett >	const_targetst

typedef std::list< irep_idt >	labelst
	Goto target labels. More...

Public Member Functions
const code_assignt &	get_assign () const
	Get the assignment for ASSIGN. More...

void	set_assign (code_assignt c)
	Set the assignment for ASSIGN. More...

const code_declt &	get_decl () const
	Get the declaration for DECL. More...

void	set_decl (code_declt c)
	Set the declaration for DECL. More...

const code_deadt &	get_dead () const
	Get the dead statement for DEAD. More...

void	set_dead (code_deadt c)
	Set the dead statement for DEAD. More...

const code_returnt &	get_return () const
	Get the return statement for READ. More...

void	set_return (code_returnt c)
	Set the return statement for READ. More...

const code_function_callt &	get_function_call () const
	Get the function call for FUNCTION_CALL. More...

void	set_function_call (code_function_callt c)
	Set the function call for FUNCTION_CALL. More...

const codet &	get_other () const
	Get the statement for OTHER. More...

void	set_other (codet &c)
	Set the statement for OTHER. More...

bool	has_condition () const
	Does this instruction have a condition? More...

const exprt &	get_condition () const
	Get the condition of gotos, assume, assert. More...

void	set_condition (exprt c)
	Set the condition of gotos, assume, assert. More...

targett	get_target () const
	Returns the first (and only) successor for the usual case of a single target. More...

void	set_target (targett t)
	Sets the first (and only) successor for the usual case of a single target. More...

bool	has_target () const

bool	is_target () const
	Is this node a branch target? More...

void	clear (goto_program_instruction_typet _type)
	Clear the node. More...

void	turn_into_skip ()
	Transforms an existing instruction into a skip, retaining the source_location. More...

	DEPRECATED (SINCE(2019, 2, 13, "use goto_programt::make_return() instead")) void make_return()

	DEPRECATED (SINCE(2019, 2, 13, "use goto_programt::make_skip() instead")) void make_skip()

	DEPRECATED (SINCE(2019, 2, 13, "use goto_programt::make_location() instead")) void make_location(const source_locationt &l)

	DEPRECATED (SINCE(2019, 2, 13, "use goto_programt::make_throw() instead")) void make_throw()

	DEPRECATED (SINCE(2019, 2, 13, "use goto_programt::make_catch() instead")) void make_catch()

	DEPRECATED (SINCE(2019, 2, 13, "use goto_programt::make_assertion() instead")) void make_assertion(const exprt &g)

	DEPRECATED (SINCE(2019, 2, 13, "use goto_programt::make_assumption() instead")) void make_assumption(const exprt &g)

	DEPRECATED (SINCE(2019, 2, 13, "use goto_programt::make_assignment() instead")) void make_assignment()

	DEPRECATED (SINCE(2019, 2, 13, "use goto_programt::make_other() instead")) void make_other(const codet &_code)

	DEPRECATED (SINCE(2019, 2, 13, "use goto_programt::make_decl() instead")) void make_decl()

	DEPRECATED (SINCE(2019, 2, 13, "use goto_programt::make_dead() instead")) void make_dead()

	DEPRECATED (SINCE(2019, 2, 13, "use goto_programt::make_atomic_begin() instead")) void make_atomic_begin()

	DEPRECATED (SINCE(2019, 2, 13, "use goto_programt::make_atomic_end() instead")) void make_atomic_end()

	DEPRECATED (SINCE(2019, 2, 13, "use goto_programt::make_end_function() instead")) void make_end_function()

	DEPRECATED (SINCE(2019, 2, 13, "use goto_programt::make_incomplete_goto() instead")) void make_incomplete_goto(const code_gotot &_code)

	DEPRECATED (SINCE(2019, 2, 13, "use goto_programt::make_goto() instead")) void make_goto(targett _target)

	DEPRECATED (SINCE(2019, 2, 13, "use goto_programt::make_goto() instead")) void make_goto(targett _target

void	complete_goto (targett _target)

	DEPRECATED (SINCE(2019, 2, 13, "use goto_programt::make_assignment() instead")) void make_assignment(const code_assignt &_code)

	DEPRECATED (SINCE(2019, 2, 13, "use goto_programt::make_decl() instead")) void make_decl(const code_declt &_code)

	DEPRECATED (SINCE(2019, 2, 13, "use goto_programt::make_function_call() instead")) void make_function_call(const code_function_callt &_code)

bool	is_goto () const

bool	is_return () const

bool	is_assign () const

bool	is_function_call () const

bool	is_throw () const

bool	is_catch () const

bool	is_skip () const

bool	is_location () const

bool	is_other () const

bool	is_decl () const

bool	is_dead () const

bool	is_assume () const

bool	is_assert () const

bool	is_atomic_begin () const

bool	is_atomic_end () const

bool	is_start_thread () const

bool	is_end_thread () const

bool	is_end_function () const

bool	is_incomplete_goto () const

	instructiont ()

	instructiont (goto_program_instruction_typet _type)

	instructiont (codet _code, source_locationt _source_location, goto_program_instruction_typet _type, exprt _guard, targetst _targets)
	Constructor that can set all members, passed by value. More...

void	swap (instructiont &instruction)
	Swap two instructions. More...

bool	is_backwards_goto () const
	Returns true if the instruction is a backwards branch. More...

std::string	to_string () const

bool	equals (const instructiont &other) const
	Syntactic equality: two instructiont are equal if they have the same type, code, guard, number of targets, and labels. More...

void	validate (const namespacet &ns, const validation_modet vm) const
	Check that the instruction is well-formed. More...

void	transform (std::function< optionalt< exprt >(exprt)>)
	Apply given transformer to all expressions; no return value means no change needed. More...

void	apply (std::function< void(const exprt &)>) const
	Apply given function to all expressions. More...

Public Attributes
codet	code
	Do not read or modify directly – use get_X() instead. More...

source_locationt	source_location
	The location of the instruction in the source file. More...

goto_program_instruction_typet	type
	What kind of instruction? More...

exprt	guard
	Guard for gotos, assume, assert Use get_condition() to read, and set_condition(c) to write. More...

targetst	targets
	The list of successor instructions. More...

labelst	labels

std::set< targett >	incoming_edges

const exprt &	g

	guard =g

unsigned	location_number = 0
	A globally unique number to identify a program location. More...

unsigned	loop_number = 0
	Number unique per function to identify loops. More...

unsigned	target_number = nil_target
	A number to identify branch targets. More...

Static Public Attributes
static const unsigned	nil_target
	Uniquely identify an invalid target or location. More...

Detailed Description

This class represents an instruction in the GOTO intermediate representation.

Three fields are key:

type: an enum value describing the action performed by this instruction
guard: an (arbitrarily complex) expression (usually an exprt) of Boolean type
code: a code statement (usually a codet)

The meaning of an instruction node depends on the type field. Different kinds of instructions make use of the fields guard and code for different purposes. We list below, using a mixture of pseudo code and plain English, the meaning of different kinds of instructions. We use guard, code, and targets to mean the value of the respective fields in this class:

GOTO: goto targets if and only if guard is true. More than one target is deprecated. Its semantics was a non-deterministic choice.
RETURN: Set the value returned by code (which shall be either nil or an instance of code_returnt) and then jump to the end of the function. Many analysis tools remove these instructions before they start.
DECL: Introduces a symbol denoted by the field code (an instance of code_declt), the life-time of which is bounded by a corresponding DEAD instruction. Non-static symbols must be DECL'd before they are used.
DEAD: Ends the life of the symbol denoted by the field code. After a DEAD instruction the symbol must be DECL'd again before use.
FUNCTION_CALL: Invoke the function denoted by field code (an instance of code_function_callt).
ASSIGN: Update the left-hand side of code (an instance of code_assignt) to the value of the right-hand side.
OTHER: Execute the code (an instance of codet of kind ID_fence, ID_printf, ID_array_copy, ID_array_set, ID_input, ID_output, ...).
ASSUME: This thread of execution waits for guard to evaluate to true. Assume does not "retro-actively" affect the thread or any ASSERTs.
ASSERT: Using ASSERT instructions is the one and only way to express properties to be verified. An assertion is true / safe if guard is true in all possible executions, otherwise it is false / unsafe. The status of the assertion does not affect execution in any way.
SKIP, LOCATION: No-op.
ATOMIC_BEGIN, ATOMIC_END: When a thread executes ATOMIC_BEGIN, no thread other will be able to execute any instruction until the same thread executes ATOMIC_END. Concurrency is not supported by all analysis tools.
END_FUNCTION: Must occur as the last instruction of the list and nowhere else.
START_THREAD: Create a new thread and run the code of this function starting from targets[0]. Quite often the instruction pointed by targets[0] will be just a FUNCTION_CALL, followed by an END_THREAD. Concurrency is not supported by all analysis tools.
END_THREAD: Terminate the calling thread. Concurrency is not supported by all analysis tools.
THROW: throw exception1, ..., exceptionN where the list of exceptions is extracted from the code field Many analysis tools remove these instructions before they start.
CATCH, when code.find(ID_exception_list) is non-empty: Establishes that from here to the next occurrence of CATCH with an empty list (see below) if
- exception1 is thrown, then goto target1,
- ...
- exceptionN is thrown, then goto targetN. The list of exceptions is obtained from the code field and the list of targets from the targets field.
CATCH, when empty code.find(ID_exception_list) is empty: clears all the catch clauses established as per the above in this function? Many analysis tools remove these instructions before they start.
INCOMPLETE GOTO: goto for which the target is yet to be determined. The target set shall be empty

Definition at line 178 of file goto_program.h.

Member Typedef Documentation

◆ const_targetst

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

Definition at line 303 of file goto_program.h.

◆ const_targett

typedef std::list<instructiont>::const_iterator goto_programt::instructiont::const_targett

Definition at line 301 of file goto_program.h.

◆ labelst

typedef std::list<irep_idt> goto_programt::instructiont::labelst

Goto target labels.

Definition at line 330 of file goto_program.h.

◆ targetst

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

Definition at line 302 of file goto_program.h.

◆ targett

typedef std::list<instructiont>::iterator goto_programt::instructiont::targett

The target for gotos and for start_thread nodes.

Definition at line 300 of file goto_program.h.

Constructor & Destructor Documentation

◆ instructiont() [1/3]

goto_programt::instructiont::instructiont ( )

inline

Definition at line 481 of file goto_program.h.

◆ instructiont() [2/3]

goto_programt::instructiont::instructiont ( goto_program_instruction_typet _type )

inlineexplicit

Definition at line 486 of file goto_program.h.

◆ instructiont() [3/3]

goto_programt::instructiont::instructiont	(	codet	_code,
		source_locationt	_source_location,
		goto_program_instruction_typet	_type,
		exprt	_guard,
		targetst	_targets
	)

inline

Constructor that can set all members, passed by value.

Definition at line 495 of file goto_program.h.

Member Function Documentation

◆ apply()

void goto_programt::instructiont::apply ( std::function< void(const exprt &)> f ) const

Apply given function to all expressions.

Definition at line 1024 of file goto_program.cpp.

◆ clear()

void goto_programt::instructiont::clear ( goto_program_instruction_typet _type )

inline

Clear the node.

Definition at line 341 of file goto_program.h.

◆ complete_goto()

void goto_programt::instructiont::complete_goto ( targett _target )

inline

Definition at line 427 of file goto_program.h.

◆ DEPRECATED() [1/20]

goto_programt::instructiont::DEPRECATED ( SINCE(2019, 2, 13, "use goto_programt::make_return() instead") )

inline

Definition at line 356 of file goto_program.h.

◆ DEPRECATED() [2/20]

goto_programt::instructiont::DEPRECATED ( SINCE(2019, 2, 13, "use goto_programt::make_skip() instead") )

inline

Definition at line 359 of file goto_program.h.

◆ DEPRECATED() [3/20]

goto_programt::instructiont::DEPRECATED ( SINCE(2019, 2, 13, "use goto_programt::make_location() instead") ) const &

inline

Definition at line 362 of file goto_program.h.

◆ DEPRECATED() [4/20]

goto_programt::instructiont::DEPRECATED ( SINCE(2019, 2, 13, "use goto_programt::make_throw() instead") )

inline

Definition at line 366 of file goto_program.h.

◆ DEPRECATED() [5/20]

goto_programt::instructiont::DEPRECATED ( SINCE(2019, 2, 13, "use goto_programt::make_catch() instead") )

inline

Definition at line 369 of file goto_program.h.

◆ DEPRECATED() [6/20]

goto_programt::instructiont::DEPRECATED ( SINCE(2019, 2, 13, "use goto_programt::make_assertion() instead") ) const &

inline

Definition at line 372 of file goto_program.h.

◆ DEPRECATED() [7/20]

goto_programt::instructiont::DEPRECATED ( SINCE(2019, 2, 13, "use goto_programt::make_assumption() instead") ) const &

inline

Definition at line 376 of file goto_program.h.

◆ DEPRECATED() [8/20]

goto_programt::instructiont::DEPRECATED ( SINCE(2019, 2, 13, "use goto_programt::make_assignment() instead") )

inline

Definition at line 380 of file goto_program.h.

◆ DEPRECATED() [9/20]

goto_programt::instructiont::DEPRECATED ( SINCE(2019, 2, 13, "use goto_programt::make_other() instead") ) const &

inline

Definition at line 384 of file goto_program.h.

◆ DEPRECATED() [10/20]

goto_programt::instructiont::DEPRECATED ( SINCE(2019, 2, 13, "use goto_programt::make_decl() instead") )

inline

Definition at line 387 of file goto_program.h.

◆ DEPRECATED() [11/20]

goto_programt::instructiont::DEPRECATED ( SINCE(2019, 2, 13, "use goto_programt::make_dead() instead") )

inline

Definition at line 390 of file goto_program.h.

◆ DEPRECATED() [12/20]

goto_programt::instructiont::DEPRECATED ( SINCE(2019, 2, 13, "use goto_programt::make_atomic_begin() instead") )

inline

Definition at line 393 of file goto_program.h.

◆ DEPRECATED() [13/20]

goto_programt::instructiont::DEPRECATED ( SINCE(2019, 2, 13, "use goto_programt::make_atomic_end() instead") )

inline

Definition at line 397 of file goto_program.h.

◆ DEPRECATED() [14/20]

goto_programt::instructiont::DEPRECATED ( SINCE(2019, 2, 13, "use goto_programt::make_end_function() instead") )

inline

Definition at line 401 of file goto_program.h.

◆ DEPRECATED() [15/20]

goto_programt::instructiont::DEPRECATED ( SINCE(2019, 2, 13, "use goto_programt::make_incomplete_goto() instead") ) const &

inline

Definition at line 405 of file goto_program.h.

◆ DEPRECATED() [16/20]

goto_programt::instructiont::DEPRECATED ( SINCE(2019, 2, 13, "use goto_programt::make_goto() instead") )

inline

Definition at line 413 of file goto_program.h.

◆ DEPRECATED() [17/20]

goto_programt::instructiont::DEPRECATED ( SINCE(2019, 2, 13, "use goto_programt::make_goto() instead") )

◆ DEPRECATED() [18/20]

goto_programt::instructiont::DEPRECATED ( SINCE(2019, 2, 13, "use goto_programt::make_assignment() instead") ) const &

inline

Definition at line 435 of file goto_program.h.

◆ DEPRECATED() [19/20]

goto_programt::instructiont::DEPRECATED ( SINCE(2019, 2, 13, "use goto_programt::make_decl() instead") ) const &

inline

Definition at line 443 of file goto_program.h.

◆ DEPRECATED() [20/20]

goto_programt::instructiont::DEPRECATED ( SINCE(2019, 2, 13, "use goto_programt::make_function_call() instead") ) const &

inline

Definition at line 450 of file goto_program.h.

◆ equals()

bool goto_programt::instructiont::equals ( const instructiont & other ) const

Syntactic equality: two instructiont are equal if they have the same type, code, guard, number of targets, and labels.

All other members can only be evaluated in the context of a goto_programt (see goto_programt::equals).

Definition at line 693 of file goto_program.cpp.

◆ get_assign()

const code_assignt& goto_programt::instructiont::get_assign ( ) const

inline

Get the assignment for ASSIGN.

Definition at line 185 of file goto_program.h.

◆ get_condition()

const exprt& goto_programt::instructiont::get_condition ( ) const

inline

Get the condition of gotos, assume, assert.

Definition at line 285 of file goto_program.h.

◆ get_dead()

const code_deadt& goto_programt::instructiont::get_dead ( ) const

inline

Get the dead statement for DEAD.

Definition at line 213 of file goto_program.h.

◆ get_decl()

const code_declt& goto_programt::instructiont::get_decl ( ) const

inline

Get the declaration for DECL.

Definition at line 199 of file goto_program.h.

◆ get_function_call()

const code_function_callt& goto_programt::instructiont::get_function_call ( ) const

inline

Get the function call for FUNCTION_CALL.

Definition at line 241 of file goto_program.h.

◆ get_other()

const codet& goto_programt::instructiont::get_other ( ) const

inline

Get the statement for OTHER.

Definition at line 255 of file goto_program.h.

◆ get_return()

const code_returnt& goto_programt::instructiont::get_return ( ) const

inline

Get the return statement for READ.

Definition at line 227 of file goto_program.h.

◆ get_target()

targett goto_programt::instructiont::get_target ( ) const

inline

Returns the first (and only) successor for the usual case of a single target.

Definition at line 310 of file goto_program.h.

◆ has_condition()

bool goto_programt::instructiont::has_condition ( ) const

inline

Does this instruction have a condition?

Definition at line 279 of file goto_program.h.

◆ has_target()

bool goto_programt::instructiont::has_target ( ) const

inline

Definition at line 324 of file goto_program.h.

◆ is_assert()

bool goto_programt::instructiont::is_assert ( ) const

inline

Definition at line 470 of file goto_program.h.

◆ is_assign()

bool goto_programt::instructiont::is_assign ( ) const

inline

Definition at line 460 of file goto_program.h.

◆ is_assume()

bool goto_programt::instructiont::is_assume ( ) const

inline

Definition at line 469 of file goto_program.h.

◆ is_atomic_begin()

bool goto_programt::instructiont::is_atomic_begin ( ) const

inline

Definition at line 471 of file goto_program.h.

◆ is_atomic_end()

bool goto_programt::instructiont::is_atomic_end ( ) const

inline

Definition at line 472 of file goto_program.h.

◆ is_backwards_goto()

bool goto_programt::instructiont::is_backwards_goto ( ) const

inline

Returns true if the instruction is a backwards branch.

Definition at line 537 of file goto_program.h.

◆ is_catch()

bool goto_programt::instructiont::is_catch ( ) const

inline

Definition at line 463 of file goto_program.h.

◆ is_dead()

bool goto_programt::instructiont::is_dead ( ) const

inline

Definition at line 468 of file goto_program.h.

◆ is_decl()

bool goto_programt::instructiont::is_decl ( ) const

inline

Definition at line 467 of file goto_program.h.

◆ is_end_function()

bool goto_programt::instructiont::is_end_function ( ) const

inline

Definition at line 475 of file goto_program.h.

◆ is_end_thread()

bool goto_programt::instructiont::is_end_thread ( ) const

inline

Definition at line 474 of file goto_program.h.

◆ is_function_call()

bool goto_programt::instructiont::is_function_call ( ) const

inline

Definition at line 461 of file goto_program.h.

◆ is_goto()

bool goto_programt::instructiont::is_goto ( ) const

inline

Definition at line 458 of file goto_program.h.

◆ is_incomplete_goto()

bool goto_programt::instructiont::is_incomplete_goto ( ) const

inline

Definition at line 476 of file goto_program.h.

◆ is_location()

bool goto_programt::instructiont::is_location ( ) const

inline

Definition at line 465 of file goto_program.h.

◆ is_other()

bool goto_programt::instructiont::is_other ( ) const

inline

Definition at line 466 of file goto_program.h.

◆ is_return()

bool goto_programt::instructiont::is_return ( ) const

inline

Definition at line 459 of file goto_program.h.

◆ is_skip()

bool goto_programt::instructiont::is_skip ( ) const

inline

Definition at line 464 of file goto_program.h.

◆ is_start_thread()

bool goto_programt::instructiont::is_start_thread ( ) const

inline

Definition at line 473 of file goto_program.h.

◆ is_target()

bool goto_programt::instructiont::is_target ( ) const

inline

Is this node a branch target?

Definition at line 337 of file goto_program.h.

◆ is_throw()

bool goto_programt::instructiont::is_throw ( ) const

inline

Definition at line 462 of file goto_program.h.

◆ set_assign()

void goto_programt::instructiont::set_assign ( code_assignt c )

inline

Set the assignment for ASSIGN.

Definition at line 192 of file goto_program.h.

◆ set_condition()

void goto_programt::instructiont::set_condition ( exprt c )

inline

Set the condition of gotos, assume, assert.

Definition at line 292 of file goto_program.h.

◆ set_dead()

void goto_programt::instructiont::set_dead ( code_deadt c )

inline

Set the dead statement for DEAD.

Definition at line 220 of file goto_program.h.

◆ set_decl()

void goto_programt::instructiont::set_decl ( code_declt c )

inline

Set the declaration for DECL.

Definition at line 206 of file goto_program.h.

◆ set_function_call()

void goto_programt::instructiont::set_function_call ( code_function_callt c )

inline

Set the function call for FUNCTION_CALL.

Definition at line 248 of file goto_program.h.

◆ set_other()

void goto_programt::instructiont::set_other ( codet & c )

inline

Set the statement for OTHER.

Definition at line 262 of file goto_program.h.

◆ set_return()

void goto_programt::instructiont::set_return ( code_returnt c )

inline

Set the return statement for READ.

Definition at line 234 of file goto_program.h.

◆ set_target()

void goto_programt::instructiont::set_target ( targett t )

inline

Sets the first (and only) successor for the usual case of a single target.

Definition at line 318 of file goto_program.h.

◆ swap()

void goto_programt::instructiont::swap ( instructiont & instruction )

inline

Swap two instructions.

Definition at line 510 of file goto_program.h.

◆ to_string()

std::string goto_programt::instructiont::to_string ( ) const

inline

Definition at line 549 of file goto_program.h.

◆ transform()

void goto_programt::instructiont::transform ( std::function< optionalt< exprt >(exprt)> f )

Apply given transformer to all expressions; no return value means no change needed.

Definition at line 906 of file goto_program.cpp.

◆ turn_into_skip()

void goto_programt::instructiont::turn_into_skip ( )

inline

Transforms an existing instruction into a skip, retaining the source_location.

Definition at line 351 of file goto_program.h.

◆ validate()

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

Check that the instruction is well-formed.

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

Definition at line 705 of file goto_program.cpp.

Member Data Documentation

◆ code

codet goto_programt::instructiont::code

Do not read or modify directly – use get_X() instead.

Definition at line 182 of file goto_program.h.

◆ g

const exprt& goto_programt::instructiont::g

Initial value:

{

make_goto(_target)

Definition at line 422 of file goto_program.h.

◆ guard [1/2]

exprt goto_programt::instructiont::guard

Guard for gotos, assume, assert Use get_condition() to read, and set_condition(c) to write.

Definition at line 276 of file goto_program.h.

◆ guard [2/2]

goto_programt::instructiont::guard =g

Definition at line 424 of file goto_program.h.

◆ incoming_edges

std::set<targett> goto_programt::instructiont::incoming_edges

Definition at line 334 of file goto_program.h.

◆ labels

labelst goto_programt::instructiont::labels

Definition at line 331 of file goto_program.h.

◆ location_number

unsigned goto_programt::instructiont::location_number = 0

A globally unique number to identify a program location.

It's guaranteed to be ordered in program order within one goto_program.

Definition at line 527 of file goto_program.h.

◆ loop_number

unsigned goto_programt::instructiont::loop_number = 0

Number unique per function to identify loops.

Definition at line 530 of file goto_program.h.

◆ nil_target

const unsigned goto_programt::instructiont::nil_target

static

Initial value:

=

std::numeric_limits<unsigned>::max()

Uniquely identify an invalid target or location.

Definition at line 521 of file goto_program.h.

◆ source_location

source_locationt goto_programt::instructiont::source_location

The location of the instruction in the source file.

Definition at line 269 of file goto_program.h.

◆ target_number

unsigned goto_programt::instructiont::target_number = nil_target

A number to identify branch targets.

This is nil_target if it's not a target.

Definition at line 534 of file goto_program.h.

◆ targets

targetst goto_programt::instructiont::targets

The list of successor instructions.

Definition at line 306 of file goto_program.h.

◆ type

goto_program_instruction_typet goto_programt::instructiont::type

What kind of instruction?

Definition at line 272 of file goto_program.h.

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

goto-programs/goto_program.h
goto-programs/goto_program.cpp

Public Types

Public Member Functions

Public Attributes

Static Public Attributes

Detailed Description

Member Typedef Documentation

◆ const_targetst

◆ const_targett

◆ labelst

◆ targetst

◆ targett

Constructor & Destructor Documentation

◆ instructiont() [1/3]

◆ instructiont() [2/3]

◆ instructiont() [3/3]

Member Function Documentation

◆ apply()

◆ clear()

◆ complete_goto()

◆ DEPRECATED() [1/20]

◆ DEPRECATED() [2/20]

◆ DEPRECATED() [3/20]

◆ DEPRECATED() [4/20]

◆ DEPRECATED() [5/20]

◆ DEPRECATED() [6/20]

◆ DEPRECATED() [7/20]

◆ DEPRECATED() [8/20]

◆ DEPRECATED() [9/20]

◆ DEPRECATED() [10/20]

◆ DEPRECATED() [11/20]

◆ DEPRECATED() [12/20]

◆ DEPRECATED() [13/20]

◆ DEPRECATED() [14/20]

◆ DEPRECATED() [15/20]

◆ DEPRECATED() [16/20]

◆ DEPRECATED() [17/20]

◆ DEPRECATED() [18/20]

◆ DEPRECATED() [19/20]

◆ DEPRECATED() [20/20]

◆ equals()

◆ get_assign()

◆ get_condition()

◆ get_dead()

◆ get_decl()

◆ get_function_call()

◆ get_other()

◆ get_return()

◆ get_target()

◆ has_condition()

◆ has_target()

◆ is_assert()

◆ is_assign()

◆ is_assume()

◆ is_atomic_begin()

◆ is_atomic_end()

◆ is_backwards_goto()

◆ is_catch()

◆ is_dead()

◆ is_decl()

◆ is_end_function()

◆ is_end_thread()

◆ is_function_call()

◆ is_goto()

◆ is_incomplete_goto()

◆ is_location()

◆ is_other()

◆ is_return()

◆ is_skip()

◆ is_start_thread()

◆ is_target()

◆ is_throw()

◆ set_assign()

◆ set_condition()

◆ set_dead()

◆ set_decl()

◆ set_function_call()

◆ set_other()

◆ set_return()

◆ set_target()

◆ swap()