CBMC
goto_programt::instructiont Class Referencefinal

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< targetttargetst
 
typedef std::list< const_targettconst_targetst
 
typedef std::list< irep_idtlabelst
 Goto target labels. More...
 

Public Member Functions

const goto_instruction_codetget_code () const
 Get the code represented by this instruction. More...
 
const goto_instruction_codetcode () const
 Get the code represented by this instruction. More...
 
goto_instruction_codetcode_nonconst ()
 Set the code represented by this instruction. More...
 
const exprtassign_lhs () const
 Get the lhs of the assignment for ASSIGN. More...
 
exprtassign_lhs_nonconst ()
 Get the lhs of the assignment for ASSIGN. More...
 
const exprtassign_rhs () const
 Get the rhs of the assignment for ASSIGN. More...
 
exprtassign_rhs_nonconst ()
 Get the rhs of the assignment for ASSIGN. More...
 
const symbol_exprtdecl_symbol () const
 Get the declared symbol for DECL. More...
 
symbol_exprtdecl_symbol ()
 Get the declared symbol for DECL. More...
 
const symbol_exprtdead_symbol () const
 Get the symbol for DEAD. More...
 
symbol_exprtdead_symbol ()
 Get the symbol for DEAD. More...
 
const exprtreturn_value () const
 Get the return value of a SET_RETURN_VALUE instruction. More...
 
exprtreturn_value ()
 Get the return value of a SET_RETURN_VALUE instruction. More...
 
const exprtcall_function () const
 Get the function that is called for FUNCTION_CALL. More...
 
exprtcall_function ()
 Get the function that is called for FUNCTION_CALL. More...
 
const exprtcall_lhs () const
 Get the lhs of a FUNCTION_CALL (may be nil) More...
 
exprtcall_lhs ()
 Get the lhs of a FUNCTION_CALL (may be nil) More...
 
const exprt::operandstcall_arguments () const
 Get the arguments of a FUNCTION_CALL. More...
 
exprt::operandstcall_arguments ()
 Get the arguments of a FUNCTION_CALL. More...
 
const goto_instruction_codetget_other () const
 Get the statement for OTHER. More...
 
void set_other (goto_instruction_codet &c)
 Set the statement for OTHER. More...
 
const source_locationtsource_location () const
 
source_locationtsource_location_nonconst ()
 
goto_program_instruction_typet type () const
 What kind of instruction? More...
 
bool has_condition () const
 Does this instruction have a condition? More...
 
const exprtcondition () const
 Get the condition of gotos, assume, assert. More...
 
exprtcondition_nonconst ()
 Get 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...
 
void turn_into_assume ()
 Transforms either an assertion or a GOTO instruction into an assumption, with the same condition. More...
 
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. 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...
 
std::ostream & output (std::ostream &) const
 Output this instruction to the given stream. More...
 

Public Attributes

targetst targets
 The list of successor instructions. More...
 
labelst labels
 
std::set< targettincoming_edges
 
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...
 

Protected Attributes

goto_instruction_codet _code
 Do not read or modify directly – use code() and code_nonconst() instead. More...
 
source_locationt _source_location
 The location of the instruction in the source file. More...
 
goto_program_instruction_typet _type
 
exprt guard
 Guard for gotos, assume, assert Use condition() method to access. 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 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

Definition at line 391 of file goto_program.h.

◆ const_targett

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

Definition at line 389 of file goto_program.h.

◆ labelst

Goto target labels.

Definition at line 418 of file goto_program.h.

◆ targetst

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

Constructor & Destructor Documentation

◆ instructiont() [1/3]

goto_programt::instructiont::instructiont ( )
inline

Definition at line 484 of file goto_program.h.

◆ instructiont() [2/3]

goto_programt::instructiont::instructiont ( goto_program_instruction_typet  __type)
inlineexplicit

Definition at line 489 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 498 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 1086 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 207 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 214 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 221 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 228 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 314 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 307 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 286 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 279 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 300 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 293 of file goto_program.h.

◆ clear()

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

Clear the node.

Definition at line 429 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 195 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 201 of file goto_program.h.

◆ complete_goto()

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

Definition at line 454 of file goto_program.h.

◆ condition()

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

Get the condition of gotos, assume, assert.

Definition at line 373 of file goto_program.h.

◆ condition_nonconst()

exprt& goto_programt::instructiont::condition_nonconst ( )
inline

Get the condition of gotos, assume, assert.

Definition at line 380 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 258 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 251 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 243 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 235 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 770 of file goto_program.cpp.

◆ get_code()

const goto_instruction_codet& goto_programt::instructiont::get_code ( ) const
inline

Get the code represented by this instruction.

Deprecated:
"deprecated since " "2021" "-" "10" "-" "12" "; " "Use code() instead"

Definition at line 189 of file goto_program.h.

◆ get_other()

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

Get the statement for OTHER.

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

◆ has_condition()

bool goto_programt::instructiont::has_condition ( ) const
inline

Does this instruction have a condition?

Definition at line 367 of file goto_program.h.

◆ has_target()

bool goto_programt::instructiont::has_target ( ) const
inline

Definition at line 412 of file goto_program.h.

◆ is_assert()

bool goto_programt::instructiont::is_assert ( ) const
inline

Definition at line 475 of file goto_program.h.

◆ is_assign()

bool goto_programt::instructiont::is_assign ( ) const
inline

Definition at line 465 of file goto_program.h.

◆ is_assume()

bool goto_programt::instructiont::is_assume ( ) const
inline

Definition at line 474 of file goto_program.h.

◆ is_atomic_begin()

bool goto_programt::instructiont::is_atomic_begin ( ) const
inline

Definition at line 476 of file goto_program.h.

◆ is_atomic_end()

bool goto_programt::instructiont::is_atomic_end ( ) const
inline

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

◆ is_catch()

bool goto_programt::instructiont::is_catch ( ) const
inline

Definition at line 468 of file goto_program.h.

◆ is_dead()

bool goto_programt::instructiont::is_dead ( ) const
inline

Definition at line 473 of file goto_program.h.

◆ is_decl()

bool goto_programt::instructiont::is_decl ( ) const
inline

Definition at line 472 of file goto_program.h.

◆ is_end_function()

bool goto_programt::instructiont::is_end_function ( ) const
inline

Definition at line 480 of file goto_program.h.

◆ is_end_thread()

bool goto_programt::instructiont::is_end_thread ( ) const
inline

Definition at line 479 of file goto_program.h.

◆ is_function_call()

bool goto_programt::instructiont::is_function_call ( ) const
inline

Definition at line 466 of file goto_program.h.

◆ is_goto()

bool goto_programt::instructiont::is_goto ( ) const
inline

Definition at line 463 of file goto_program.h.

◆ is_incomplete_goto()

bool goto_programt::instructiont::is_incomplete_goto ( ) const
inline

Definition at line 481 of file goto_program.h.

◆ is_location()

bool goto_programt::instructiont::is_location ( ) const
inline

Definition at line 470 of file goto_program.h.

◆ is_other()

bool goto_programt::instructiont::is_other ( ) const
inline

Definition at line 471 of file goto_program.h.

◆ is_set_return_value()

bool goto_programt::instructiont::is_set_return_value ( ) const
inline

Definition at line 464 of file goto_program.h.

◆ is_skip()

bool goto_programt::instructiont::is_skip ( ) const
inline

Definition at line 469 of file goto_program.h.

◆ is_start_thread()

bool goto_programt::instructiont::is_start_thread ( ) const
inline

Definition at line 478 of file goto_program.h.

◆ is_target()

bool goto_programt::instructiont::is_target ( ) const
inline

Is this node a branch target?

Definition at line 425 of file goto_program.h.

◆ is_throw()

bool goto_programt::instructiont::is_throw ( ) const
inline

Definition at line 467 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
outthe stream to write the goto string to
Returns
Appends to out a two line representation of the instruction

Definition at line 47 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 272 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 265 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 328 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 406 of file goto_program.h.

◆ source_location()

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

Definition at line 340 of file goto_program.h.

◆ source_location_nonconst()

source_locationt& goto_programt::instructiont::source_location_nonconst ( )
inline

Definition at line 345 of file goto_program.h.

◆ swap()

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

Swap two instructions.

Definition at line 513 of file goto_program.h.

◆ to_string()

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

Definition at line 553 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 982 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 446 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 439 of file goto_program.h.

◆ type()

goto_program_instruction_typet goto_programt::instructiont::type ( ) const
inline

What kind of instruction?

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

◆ _type

goto_program_instruction_typet goto_programt::instructiont::_type
protected

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

◆ incoming_edges

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

Definition at line 422 of file goto_program.h.

◆ labels

labelst goto_programt::instructiont::labels

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

◆ loop_number

unsigned goto_programt::instructiont::loop_number = 0

Number unique per function to identify loops.

Definition at line 534 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 525 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 538 of file goto_program.h.

◆ targets

targetst goto_programt::instructiont::targets

The list of successor instructions.

Definition at line 394 of file goto_program.h.


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