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

#include <goto_program.h>

Collaboration diagram for goto_programt::instructiont:

Classes
struct	target_less_than
	A total order over `targett` and `const_targett`. More...

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

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.

Public Member Functions
const goto_instruction_codet &	code () const
	Get the code represented by this instruction.

goto_instruction_codet &	code_nonconst ()
	Set the code represented by this instruction.

const exprt &	assign_lhs () const
	Get the lhs of the assignment for ASSIGN.

exprt &	assign_lhs_nonconst ()
	Get the lhs of the assignment for ASSIGN.

const exprt &	assign_rhs () const
	Get the rhs of the assignment for ASSIGN.

exprt &	assign_rhs_nonconst ()
	Get the rhs of the assignment for ASSIGN.

const symbol_exprt &	decl_symbol () const
	Get the declared symbol for DECL.

symbol_exprt &	decl_symbol ()
	Get the declared symbol for DECL.

const symbol_exprt &	dead_symbol () const
	Get the symbol for DEAD.

symbol_exprt &	dead_symbol ()
	Get the symbol for DEAD.

const exprt &	return_value () const
	Get the return value of a SET_RETURN_VALUE instruction.

exprt &	return_value ()
	Get the return value of a SET_RETURN_VALUE instruction.

const exprt &	call_function () const
	Get the function that is called for FUNCTION_CALL.

exprt &	call_function ()
	Get the function that is called for FUNCTION_CALL.

const exprt &	call_lhs () const
	Get the lhs of a FUNCTION_CALL (may be nil)

exprt &	call_lhs ()
	Get the lhs of a FUNCTION_CALL (may be nil)

const exprt::operandst &	call_arguments () const
	Get the arguments of a FUNCTION_CALL.

exprt::operandst &	call_arguments ()
	Get the arguments of a FUNCTION_CALL.

const goto_instruction_codet &	get_other () const
	Get the statement for OTHER.

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

const source_locationt &	source_location () const

source_locationt &	source_location_nonconst ()

goto_program_instruction_typet	type () const
	What kind of instruction?

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

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

exprt &	condition_nonconst ()
	Get the condition of gotos, assume, assert.

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

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

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

bool	has_target () const

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

void	clear (goto_program_instruction_typet __type)
	Clear the node.

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

void	turn_into_assume ()
	Transforms either an assertion or a GOTO instruction into an assumption, with the same condition.

void	complete_goto (targett _target)

bool	is_goto () const

bool	is_set_return_value () 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 (goto_instruction_codet __code, source_locationt __source_location, goto_program_instruction_typet __type, exprt _guard, targetst _targets)
	Constructor that can set all members, passed by value.

void	swap (instructiont &instruction)
	Swap two instructions.

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

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.

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

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

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

std::ostream &	output (std::ostream &) const
	Output this instruction to the given stream.

Public Attributes
targetst	targets
	The list of successor instructions.

labelst	labels

std::set< targett, target_less_than >	incoming_edges

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

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

unsigned	target_number = nil_target
	A number to identify branch targets.

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

Protected Attributes
goto_instruction_codet	_code
	Do not read or modify directly – use code() and code_nonconst() instead.

source_locationt	_source_location
	The location of the instruction in the source file.

goto_program_instruction_typet	_type

exprt	guard
	Guard for gotos, assume, assert Use condition() method to access.

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 goto_instruction_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.
SET_RETURN_VALUE: Set the value returned by return_value(). The control flow is not altered. 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 returned by call_function with the arguments returned by call_arguments, then assign the return value (if any) to call_lhs
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 goto_instruction_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 180 of file goto_program.h.

Member Typedef Documentation

◆ const_targetst

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

Definition at line 384 of file goto_program.h.

◆ const_targett

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

Definition at line 382 of file goto_program.h.

◆ labelst

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

Goto target labels.

Definition at line 446 of file goto_program.h.

◆ targetst

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

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

Constructor & Destructor Documentation

◆ instructiont() [1/3]

goto_programt::instructiont::instructiont ( )

inline

Definition at line 512 of file goto_program.h.

◆ instructiont() [2/3]

goto_programt::instructiont::instructiont ( goto_program_instruction_typet __type )

inlineexplicit

Definition at line 517 of file goto_program.h.

◆ instructiont() [3/3]

goto_programt::instructiont::instructiont	(	goto_instruction_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 526 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 1088 of file goto_program.cpp.

◆ assign_lhs()

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

inline

Get the lhs of the assignment for ASSIGN.

Definition at line 200 of file goto_program.h.

◆ assign_lhs_nonconst()

exprt & goto_programt::instructiont::assign_lhs_nonconst ( )

inline

Get the lhs of the assignment for ASSIGN.

Definition at line 207 of file goto_program.h.

◆ assign_rhs()

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

inline

Get the rhs of the assignment for ASSIGN.

Definition at line 214 of file goto_program.h.

◆ assign_rhs_nonconst()

exprt & goto_programt::instructiont::assign_rhs_nonconst ( )

inline

Get the rhs of the assignment for ASSIGN.

Definition at line 221 of file goto_program.h.

◆ call_arguments() [1/2]

exprt::operandst & goto_programt::instructiont::call_arguments ( )

inline

Get the arguments of a FUNCTION_CALL.

Definition at line 307 of file goto_program.h.

◆ call_arguments() [2/2]

const exprt::operandst & goto_programt::instructiont::call_arguments ( ) const

inline

Get the arguments of a FUNCTION_CALL.

Definition at line 300 of file goto_program.h.

◆ call_function() [1/2]

exprt & goto_programt::instructiont::call_function ( )

inline

Get the function that is called for FUNCTION_CALL.

Definition at line 279 of file goto_program.h.

◆ call_function() [2/2]

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

inline

Get the function that is called for FUNCTION_CALL.

Definition at line 272 of file goto_program.h.

◆ call_lhs() [1/2]

exprt & goto_programt::instructiont::call_lhs ( )

inline

Get the lhs of a FUNCTION_CALL (may be nil)

Definition at line 293 of file goto_program.h.

◆ call_lhs() [2/2]

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

inline

Get the lhs of a FUNCTION_CALL (may be nil)

Definition at line 286 of file goto_program.h.

◆ clear()

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

inline

Clear the node.

Definition at line 457 of file goto_program.h.

◆ code()

const goto_instruction_codet & goto_programt::instructiont::code ( ) const

inline

Get the code represented by this instruction.

Definition at line 188 of file goto_program.h.

◆ code_nonconst()

goto_instruction_codet & goto_programt::instructiont::code_nonconst ( )

inline

Set the code represented by this instruction.

Definition at line 194 of file goto_program.h.

◆ complete_goto()

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

inline

Definition at line 482 of file goto_program.h.

◆ condition()

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

inline

Get the condition of gotos, assume, assert.

Definition at line 366 of file goto_program.h.

◆ condition_nonconst()

exprt & goto_programt::instructiont::condition_nonconst ( )

inline

Get the condition of gotos, assume, assert.

Definition at line 373 of file goto_program.h.

◆ dead_symbol() [1/2]

symbol_exprt & goto_programt::instructiont::dead_symbol ( )

inline

Get the symbol for DEAD.

Definition at line 251 of file goto_program.h.

◆ dead_symbol() [2/2]

const symbol_exprt & goto_programt::instructiont::dead_symbol ( ) const

inline

Get the symbol for DEAD.

Definition at line 244 of file goto_program.h.

◆ decl_symbol() [1/2]

symbol_exprt & goto_programt::instructiont::decl_symbol ( )

inline

Get the declared symbol for DECL.

Definition at line 236 of file goto_program.h.

◆ decl_symbol() [2/2]

const symbol_exprt & goto_programt::instructiont::decl_symbol ( ) const

inline

Get the declared symbol for DECL.

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

◆ get_other()

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

inline

Get the statement for OTHER.

Definition at line 314 of file goto_program.h.

◆ get_target() [1/2]

targett goto_programt::instructiont::get_target ( )

inline

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

Definition at line 426 of file goto_program.h.

◆ get_target() [2/2]

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

◆ has_condition()

bool goto_programt::instructiont::has_condition ( ) const

inline

Does this instruction have a condition?

Definition at line 360 of file goto_program.h.

◆ has_target()

bool goto_programt::instructiont::has_target ( ) const

inline

Definition at line 440 of file goto_program.h.

◆ is_assert()

bool goto_programt::instructiont::is_assert ( ) const

inline

Definition at line 503 of file goto_program.h.

◆ is_assign()

bool goto_programt::instructiont::is_assign ( ) const

inline

Definition at line 493 of file goto_program.h.

◆ is_assume()

bool goto_programt::instructiont::is_assume ( ) const

inline

Definition at line 502 of file goto_program.h.

◆ is_atomic_begin()

bool goto_programt::instructiont::is_atomic_begin ( ) const

inline

Definition at line 504 of file goto_program.h.

◆ is_atomic_end()

bool goto_programt::instructiont::is_atomic_end ( ) const

inline

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

◆ is_catch()

bool goto_programt::instructiont::is_catch ( ) const

inline

Definition at line 496 of file goto_program.h.

◆ is_dead()

bool goto_programt::instructiont::is_dead ( ) const

inline

Definition at line 501 of file goto_program.h.

◆ is_decl()

bool goto_programt::instructiont::is_decl ( ) const

inline

Definition at line 500 of file goto_program.h.

◆ is_end_function()

bool goto_programt::instructiont::is_end_function ( ) const

inline

Definition at line 508 of file goto_program.h.

◆ is_end_thread()

bool goto_programt::instructiont::is_end_thread ( ) const

inline

Definition at line 507 of file goto_program.h.

◆ is_function_call()

bool goto_programt::instructiont::is_function_call ( ) const

inline

Definition at line 494 of file goto_program.h.

◆ is_goto()

bool goto_programt::instructiont::is_goto ( ) const

inline

Definition at line 491 of file goto_program.h.

◆ is_incomplete_goto()

bool goto_programt::instructiont::is_incomplete_goto ( ) const

inline

Definition at line 509 of file goto_program.h.

◆ is_location()

bool goto_programt::instructiont::is_location ( ) const

inline

Definition at line 498 of file goto_program.h.

◆ is_other()

bool goto_programt::instructiont::is_other ( ) const

inline

Definition at line 499 of file goto_program.h.

◆ is_set_return_value()

bool goto_programt::instructiont::is_set_return_value ( ) const

inline

Definition at line 492 of file goto_program.h.

◆ is_skip()

bool goto_programt::instructiont::is_skip ( ) const

inline

Definition at line 497 of file goto_program.h.

◆ is_start_thread()

bool goto_programt::instructiont::is_start_thread ( ) const

inline

Definition at line 506 of file goto_program.h.

◆ is_target()

bool goto_programt::instructiont::is_target ( ) const

inline

Is this node a branch target?

Definition at line 453 of file goto_program.h.

◆ is_throw()

bool goto_programt::instructiont::is_throw ( ) const

inline

Definition at line 495 of file goto_program.h.

◆ output()

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

Output this instruction to the given stream.

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

out	the stream to write the goto string to

Returns: Appends to out a two line representation of the instruction

Definition at line 49 of file goto_program.cpp.

◆ return_value() [1/2]

exprt & goto_programt::instructiont::return_value ( )

inline

Get the return value of a SET_RETURN_VALUE instruction.

Definition at line 265 of file goto_program.h.

◆ return_value() [2/2]

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

inline

Get the return value of a SET_RETURN_VALUE instruction.

Definition at line 258 of file goto_program.h.

◆ set_other()

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

inline

Set the statement for OTHER.

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

◆ source_location()

const source_locationt & goto_programt::instructiont::source_location ( ) const

inline

Definition at line 333 of file goto_program.h.

◆ source_location_nonconst()

source_locationt & goto_programt::instructiont::source_location_nonconst ( )

inline

Definition at line 338 of file goto_program.h.

◆ swap()

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

inline

Swap two instructions.

Definition at line 541 of file goto_program.h.

◆ to_string()

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

inline

Definition at line 581 of file goto_program.h.

◆ transform()

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

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

Definition at line 984 of file goto_program.cpp.

◆ turn_into_assume()

void goto_programt::instructiont::turn_into_assume ( )

inline

Transforms either an assertion or a GOTO instruction into an assumption, with the same condition.

Definition at line 474 of file goto_program.h.

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

◆ type()

goto_program_instruction_typet goto_programt::instructiont::type ( ) const

inline

What kind of instruction?

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

Member Data Documentation

◆ _code

goto_instruction_codet goto_programt::instructiont::_code

protected

Do not read or modify directly – use code() and code_nonconst() instead.

Definition at line 184 of file goto_program.h.

◆ _source_location

source_locationt goto_programt::instructiont::_source_location

protected

The location of the instruction in the source file.

Use source_location() to access.

Definition at line 330 of file goto_program.h.

◆ _type

goto_program_instruction_typet goto_programt::instructiont::_type

protected

Definition at line 352 of file goto_program.h.

◆ guard

exprt goto_programt::instructiont::guard

protected

Guard for gotos, assume, assert Use condition() method to access.

Definition at line 356 of file goto_program.h.

◆ incoming_edges

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

Definition at line 450 of file goto_program.h.

◆ labels

labelst goto_programt::instructiont::labels

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

◆ loop_number

unsigned goto_programt::instructiont::loop_number = 0

Number unique per function to identify loops.

Definition at line 562 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 553 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 566 of file goto_program.h.

◆ targets

targetst goto_programt::instructiont::targets

The list of successor instructions.

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

Public Attributes

Static Public Attributes

Protected 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()

◆ assign_lhs()

◆ assign_lhs_nonconst()

◆ assign_rhs()

◆ assign_rhs_nonconst()

◆ call_arguments() [1/2]

◆ call_arguments() [2/2]

◆ call_function() [1/2]

◆ call_function() [2/2]

◆ call_lhs() [1/2]

◆ call_lhs() [2/2]

◆ clear()

◆ code()

◆ code_nonconst()

◆ complete_goto()

◆ condition()

◆ condition_nonconst()

◆ dead_symbol() [1/2]

◆ dead_symbol() [2/2]

◆ decl_symbol() [1/2]

◆ decl_symbol() [2/2]

◆ equals()

◆ get_other()

◆ get_target() [1/2]

◆ get_target() [2/2]

◆ 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_set_return_value()

◆ is_skip()

◆ is_start_thread()

◆ is_target()

◆ is_throw()

◆ output()

◆ return_value() [1/2]

◆ return_value() [2/2]

◆ set_other()

◆ set_target()

◆ source_location()

◆ source_location_nonconst()

◆ swap()

◆ to_string()

◆ transform()

◆ turn_into_assume()

◆ turn_into_skip()

◆ type()

◆ validate()