cprover
Public Types | Public Member Functions | Public Attributes | Static Public Attributes | List of all members
goto_program_templatet< codeT, guardT >::instructiont Class Reference

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

#include <goto_program_template.h>

Collaboration diagram for goto_program_templatet< codeT, guardT >::instructiont:
[legend]

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

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 is_target () const
 Is this node a branch target? More...
 
void clear (goto_program_instruction_typet _type)
 Clear the node. More...
 
void make_goto ()
 
void make_return ()
 
void make_skip ()
 
void make_throw ()
 
void make_catch ()
 
void make_assertion (const guardT &g)
 
void make_assumption (const guardT &g)
 
void make_assignment ()
 
void make_other (const codeT &_code)
 
void make_decl ()
 
void make_dead ()
 
void make_atomic_begin ()
 
void make_atomic_end ()
 
void make_goto (targett _target)
 
void make_goto (targett _target, const guardT &g)
 
void make_function_call (const codeT &_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
 
 instructiont ()
 
 instructiont (goto_program_instruction_typet _type)
 
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
 

Public Attributes

codeT code
 
irep_idt function
 The function this instruction belongs to. 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...
 
guardT guard
 Guard for gotos, assume, assert. More...
 
targetst targets
 The list of successor instructions. More...
 
labelst labels
 
std::set< targett > incoming_edges
 
unsigned location_number
 A globally unique number to identify a program location. More...
 
unsigned loop_number
 Number unique per function to identify loops. More...
 
unsigned target_number
 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

template<class codeT, class guardT>
class goto_program_templatet< codeT, guardT >::instructiont

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: if guard then goto targets
  • 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.
  • 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.
  • 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: Wait for guard to evaluate to true.
  • ASSERT: Using ASSERT instructions is the one and only way to express properties to be verified. Execution paths abort if guard evaluates to false.
  • 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.
  • END_FUNCTION: Can only occur as the last instruction of the list.
  • 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.
  • END_THREAD: Terminate the calling thread.
  • THROW: throw exception1, ..., exceptionN where the list of exceptions is extracted from the code field
  • 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?

Definition at line 159 of file goto_program_template.h.

Member Typedef Documentation

◆ const_targetst

template<class codeT, class guardT>
typedef std::list<const_targett> goto_program_templatet< codeT, guardT >::instructiont::const_targetst

Definition at line 181 of file goto_program_template.h.

◆ const_targett

template<class codeT, class guardT>
typedef std::list<instructiont>::const_iterator goto_program_templatet< codeT, guardT >::instructiont::const_targett

Definition at line 179 of file goto_program_template.h.

◆ labelst

template<class codeT, class guardT>
typedef std::list<irep_idt> goto_program_templatet< codeT, guardT >::instructiont::labelst

Goto target labels.

Definition at line 203 of file goto_program_template.h.

◆ targetst

template<class codeT, class guardT>
typedef std::list<targett> goto_program_templatet< codeT, guardT >::instructiont::targetst

Definition at line 180 of file goto_program_template.h.

◆ targett

template<class codeT, class guardT>
typedef std::list<instructiont>::iterator goto_program_templatet< codeT, guardT >::instructiont::targett

The target for gotos and for start_thread nodes.

Definition at line 178 of file goto_program_template.h.

Constructor & Destructor Documentation

◆ instructiont() [1/2]

template<class codeT, class guardT>
goto_program_templatet< codeT, guardT >::instructiont::instructiont ( )
inline

Definition at line 273 of file goto_program_template.h.

◆ instructiont() [2/2]

template<class codeT, class guardT>
goto_program_templatet< codeT, guardT >::instructiont::instructiont ( goto_program_instruction_typet  _type)
inlineexplicit

Definition at line 278 of file goto_program_template.h.

Member Function Documentation

◆ clear()

template<class codeT, class guardT>
void goto_program_templatet< codeT, guardT >::instructiont::clear ( goto_program_instruction_typet  _type)
inline

Clear the node.

Definition at line 214 of file goto_program_template.h.

References goto_program_templatet< codeT, guardT >::instructiont::code, goto_program_templatet< codeT, guardT >::instructiont::guard, goto_program_templatet< codeT, guardT >::instructiont::targets, and goto_program_templatet< codeT, guardT >::instructiont::type.

Referenced by goto_program_templatet< codeT, guardT >::instructiont::make_assertion(), goto_program_templatet< codeT, guardT >::instructiont::make_assignment(), goto_program_templatet< codeT, guardT >::instructiont::make_assumption(), goto_program_templatet< codeT, guardT >::instructiont::make_atomic_begin(), goto_program_templatet< codeT, guardT >::instructiont::make_atomic_end(), goto_program_templatet< codeT, guardT >::instructiont::make_catch(), goto_program_templatet< codeT, guardT >::instructiont::make_dead(), goto_program_templatet< codeT, guardT >::instructiont::make_decl(), goto_program_templatet< codeT, guardT >::instructiont::make_function_call(), goto_program_templatet< codeT, guardT >::instructiont::make_goto(), goto_program_templatet< codeT, guardT >::instructiont::make_other(), goto_program_templatet< codeT, guardT >::instructiont::make_return(), goto_program_templatet< codeT, guardT >::instructiont::make_skip(), and goto_program_templatet< codeT, guardT >::instructiont::make_throw().

◆ get_target()

template<class codeT, class guardT>
targett goto_program_templatet< codeT, guardT >::instructiont::get_target ( ) const
inline

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

Definition at line 188 of file goto_program_template.h.

References goto_program_templatet< codeT, guardT >::instructiont::targets.

◆ is_assert()

template<class codeT, class guardT>
bool goto_program_templatet< codeT, guardT >::instructiont::is_assert ( ) const
inline

Definition at line 266 of file goto_program_template.h.

References ASSERT, and goto_program_templatet< codeT, guardT >::instructiont::type.

◆ is_assign()

template<class codeT, class guardT>
bool goto_program_templatet< codeT, guardT >::instructiont::is_assign ( ) const
inline

Definition at line 256 of file goto_program_template.h.

References ASSIGN, and goto_program_templatet< codeT, guardT >::instructiont::type.

◆ is_assume()

template<class codeT, class guardT>
bool goto_program_templatet< codeT, guardT >::instructiont::is_assume ( ) const
inline

Definition at line 265 of file goto_program_template.h.

References ASSUME, and goto_program_templatet< codeT, guardT >::instructiont::type.

◆ is_atomic_begin()

template<class codeT, class guardT>
bool goto_program_templatet< codeT, guardT >::instructiont::is_atomic_begin ( ) const
inline

Definition at line 267 of file goto_program_template.h.

References ATOMIC_BEGIN, and goto_program_templatet< codeT, guardT >::instructiont::type.

◆ is_atomic_end()

template<class codeT, class guardT>
bool goto_program_templatet< codeT, guardT >::instructiont::is_atomic_end ( ) const
inline

Definition at line 268 of file goto_program_template.h.

References ATOMIC_END, and goto_program_templatet< codeT, guardT >::instructiont::type.

◆ is_backwards_goto()

template<class codeT, class guardT>
bool goto_program_templatet< codeT, guardT >::instructiont::is_backwards_goto ( ) const
inline

Returns true if the instruction is a backwards branch.

Definition at line 324 of file goto_program_template.h.

References goto_program_templatet< codeT, guardT >::instructiont::is_goto(), goto_program_templatet< codeT, guardT >::instructiont::location_number, and goto_program_templatet< codeT, guardT >::instructiont::targets.

◆ is_catch()

template<class codeT, class guardT>
bool goto_program_templatet< codeT, guardT >::instructiont::is_catch ( ) const
inline

Definition at line 259 of file goto_program_template.h.

References CATCH, and goto_program_templatet< codeT, guardT >::instructiont::type.

◆ is_dead()

template<class codeT, class guardT>
bool goto_program_templatet< codeT, guardT >::instructiont::is_dead ( ) const
inline

Definition at line 264 of file goto_program_template.h.

References DEAD, and goto_program_templatet< codeT, guardT >::instructiont::type.

◆ is_decl()

template<class codeT, class guardT>
bool goto_program_templatet< codeT, guardT >::instructiont::is_decl ( ) const
inline

Definition at line 263 of file goto_program_template.h.

References DECL, and goto_program_templatet< codeT, guardT >::instructiont::type.

◆ is_end_function()

template<class codeT, class guardT>
bool goto_program_templatet< codeT, guardT >::instructiont::is_end_function ( ) const
inline

Definition at line 271 of file goto_program_template.h.

References END_FUNCTION, and goto_program_templatet< codeT, guardT >::instructiont::type.

◆ is_end_thread()

template<class codeT, class guardT>
bool goto_program_templatet< codeT, guardT >::instructiont::is_end_thread ( ) const
inline

Definition at line 270 of file goto_program_template.h.

References END_THREAD, and goto_program_templatet< codeT, guardT >::instructiont::type.

◆ is_function_call()

template<class codeT, class guardT>
bool goto_program_templatet< codeT, guardT >::instructiont::is_function_call ( ) const
inline

Definition at line 257 of file goto_program_template.h.

References FUNCTION_CALL, and goto_program_templatet< codeT, guardT >::instructiont::type.

◆ is_goto()

template<class codeT, class guardT>
bool goto_program_templatet< codeT, guardT >::instructiont::is_goto ( ) const
inline

Definition at line 254 of file goto_program_template.h.

References GOTO, and goto_program_templatet< codeT, guardT >::instructiont::type.

Referenced by goto_program_templatet< codeT, guardT >::instructiont::is_backwards_goto().

◆ is_location()

template<class codeT, class guardT>
bool goto_program_templatet< codeT, guardT >::instructiont::is_location ( ) const
inline

Definition at line 261 of file goto_program_template.h.

References LOCATION, and goto_program_templatet< codeT, guardT >::instructiont::type.

◆ is_other()

template<class codeT, class guardT>
bool goto_program_templatet< codeT, guardT >::instructiont::is_other ( ) const
inline

Definition at line 262 of file goto_program_template.h.

References OTHER, and goto_program_templatet< codeT, guardT >::instructiont::type.

◆ is_return()

template<class codeT, class guardT>
bool goto_program_templatet< codeT, guardT >::instructiont::is_return ( ) const
inline

Definition at line 255 of file goto_program_template.h.

References RETURN, and goto_program_templatet< codeT, guardT >::instructiont::type.

◆ is_skip()

template<class codeT, class guardT>
bool goto_program_templatet< codeT, guardT >::instructiont::is_skip ( ) const
inline

Definition at line 260 of file goto_program_template.h.

References SKIP, and goto_program_templatet< codeT, guardT >::instructiont::type.

◆ is_start_thread()

template<class codeT, class guardT>
bool goto_program_templatet< codeT, guardT >::instructiont::is_start_thread ( ) const
inline

Definition at line 269 of file goto_program_template.h.

References START_THREAD, and goto_program_templatet< codeT, guardT >::instructiont::type.

◆ is_target()

template<class codeT, class guardT>
bool goto_program_templatet< codeT, guardT >::instructiont::is_target ( ) const
inline

Is this node a branch target?

Definition at line 210 of file goto_program_template.h.

References goto_program_templatet< codeT, guardT >::instructiont::nil_target, and goto_program_templatet< codeT, guardT >::instructiont::target_number.

◆ is_throw()

template<class codeT, class guardT>
bool goto_program_templatet< codeT, guardT >::instructiont::is_throw ( ) const
inline

Definition at line 258 of file goto_program_template.h.

References THROW, and goto_program_templatet< codeT, guardT >::instructiont::type.

◆ make_assertion()

template<class codeT, class guardT>
void goto_program_templatet< codeT, guardT >::instructiont::make_assertion ( const guardT &  g)
inline

Definition at line 227 of file goto_program_template.h.

References ASSERT, goto_program_templatet< codeT, guardT >::instructiont::clear(), and goto_program_templatet< codeT, guardT >::instructiont::guard.

◆ make_assignment()

template<class codeT, class guardT>
void goto_program_templatet< codeT, guardT >::instructiont::make_assignment ( )
inline

Definition at line 229 of file goto_program_template.h.

References ASSIGN, and goto_program_templatet< codeT, guardT >::instructiont::clear().

◆ make_assumption()

template<class codeT, class guardT>
void goto_program_templatet< codeT, guardT >::instructiont::make_assumption ( const guardT &  g)
inline

Definition at line 228 of file goto_program_template.h.

References ASSUME, goto_program_templatet< codeT, guardT >::instructiont::clear(), and goto_program_templatet< codeT, guardT >::instructiont::guard.

◆ make_atomic_begin()

template<class codeT, class guardT>
void goto_program_templatet< codeT, guardT >::instructiont::make_atomic_begin ( )
inline

Definition at line 233 of file goto_program_template.h.

References ATOMIC_BEGIN, and goto_program_templatet< codeT, guardT >::instructiont::clear().

◆ make_atomic_end()

template<class codeT, class guardT>
void goto_program_templatet< codeT, guardT >::instructiont::make_atomic_end ( )
inline

Definition at line 234 of file goto_program_template.h.

References ATOMIC_END, and goto_program_templatet< codeT, guardT >::instructiont::clear().

◆ make_catch()

template<class codeT, class guardT>
void goto_program_templatet< codeT, guardT >::instructiont::make_catch ( )
inline

Definition at line 226 of file goto_program_template.h.

References CATCH, and goto_program_templatet< codeT, guardT >::instructiont::clear().

◆ make_dead()

template<class codeT, class guardT>
void goto_program_templatet< codeT, guardT >::instructiont::make_dead ( )
inline

Definition at line 232 of file goto_program_template.h.

References goto_program_templatet< codeT, guardT >::instructiont::clear(), and DEAD.

◆ make_decl()

template<class codeT, class guardT>
void goto_program_templatet< codeT, guardT >::instructiont::make_decl ( )
inline

Definition at line 231 of file goto_program_template.h.

References goto_program_templatet< codeT, guardT >::instructiont::clear(), and DECL.

◆ make_function_call()

template<class codeT, class guardT>
void goto_program_templatet< codeT, guardT >::instructiont::make_function_call ( const codeT &  _code)
inline

Definition at line 248 of file goto_program_template.h.

References goto_program_templatet< codeT, guardT >::instructiont::clear(), goto_program_templatet< codeT, guardT >::instructiont::code, and FUNCTION_CALL.

◆ make_goto() [1/3]

template<class codeT, class guardT>
void goto_program_templatet< codeT, guardT >::instructiont::make_goto ( )
inline

Definition at line 222 of file goto_program_template.h.

References goto_program_templatet< codeT, guardT >::instructiont::clear(), and GOTO.

Referenced by goto_program_templatet< codeT, guardT >::instructiont::make_goto().

◆ make_goto() [2/3]

template<class codeT, class guardT>
void goto_program_templatet< codeT, guardT >::instructiont::make_goto ( targett  _target)
inline

Definition at line 236 of file goto_program_template.h.

References goto_program_templatet< codeT, guardT >::instructiont::make_goto(), and goto_program_templatet< codeT, guardT >::instructiont::targets.

◆ make_goto() [3/3]

template<class codeT, class guardT>
void goto_program_templatet< codeT, guardT >::instructiont::make_goto ( targett  _target,
const guardT &  g 
)
inline

Definition at line 242 of file goto_program_template.h.

References goto_program_templatet< codeT, guardT >::instructiont::guard, and goto_program_templatet< codeT, guardT >::instructiont::make_goto().

◆ make_other()

template<class codeT, class guardT>
void goto_program_templatet< codeT, guardT >::instructiont::make_other ( const codeT &  _code)
inline

Definition at line 230 of file goto_program_template.h.

References goto_program_templatet< codeT, guardT >::instructiont::clear(), goto_program_templatet< codeT, guardT >::instructiont::code, and OTHER.

◆ make_return()

template<class codeT, class guardT>
void goto_program_templatet< codeT, guardT >::instructiont::make_return ( )
inline

Definition at line 223 of file goto_program_template.h.

References goto_program_templatet< codeT, guardT >::instructiont::clear(), and RETURN.

◆ make_skip()

template<class codeT, class guardT>
void goto_program_templatet< codeT, guardT >::instructiont::make_skip ( )
inline

Definition at line 224 of file goto_program_template.h.

References goto_program_templatet< codeT, guardT >::instructiont::clear(), and SKIP.

◆ make_throw()

template<class codeT, class guardT>
void goto_program_templatet< codeT, guardT >::instructiont::make_throw ( )
inline

Definition at line 225 of file goto_program_template.h.

References goto_program_templatet< codeT, guardT >::instructiont::clear(), and THROW.

◆ set_target()

template<class codeT, class guardT>
void goto_program_templatet< codeT, guardT >::instructiont::set_target ( targett  t)
inline

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

Definition at line 196 of file goto_program_template.h.

References goto_program_templatet< codeT, guardT >::instructiont::targets.

◆ swap()

template<class codeT, class guardT>
void goto_program_templatet< codeT, guardT >::instructiont::swap ( instructiont &  instruction)
inline

Swap two instructions.

Definition at line 289 of file goto_program_template.h.

References goto_program_templatet< codeT, guardT >::instructiont::code, goto_program_templatet< codeT, guardT >::instructiont::function, goto_program_templatet< codeT, guardT >::instructiont::guard, goto_program_templatet< codeT, guardT >::instructiont::source_location, goto_program_templatet< codeT, guardT >::instructiont::targets, and goto_program_templatet< codeT, guardT >::instructiont::type.

◆ to_string()

template<class codeT, class guardT>
std::string goto_program_templatet< codeT, guardT >::instructiont::to_string ( ) const
inline

Definition at line 336 of file goto_program_template.h.

References goto_program_templatet< codeT, guardT >::instructiont::type.

Member Data Documentation

◆ code

template<class codeT, class guardT>
codeT goto_program_templatet< codeT, guardT >::instructiont::code

Definition at line 162 of file goto_program_template.h.

Referenced by goto_program_templatet< codeT, guardT >::instructiont::clear(), goto_program_templatet< codeT, guardT >::instructiont::make_function_call(), goto_program_templatet< codeT, guardT >::instructiont::make_other(), and goto_program_templatet< codeT, guardT >::instructiont::swap().

◆ function

template<class codeT, class guardT>
irep_idt goto_program_templatet< codeT, guardT >::instructiont::function

The function this instruction belongs to.

Definition at line 165 of file goto_program_template.h.

Referenced by goto_program_templatet< codeT, guardT >::instructiont::swap().

◆ guard

template<class codeT, class guardT>
guardT goto_program_templatet< codeT, guardT >::instructiont::guard

Guard for gotos, assume, assert.

Definition at line 174 of file goto_program_template.h.

Referenced by goto_program_templatet< codeT, guardT >::instructiont::clear(), goto_program_templatet< codeT, guardT >::instructiont::make_assertion(), goto_program_templatet< codeT, guardT >::instructiont::make_assumption(), goto_program_templatet< codeT, guardT >::instructiont::make_goto(), and goto_program_templatet< codeT, guardT >::instructiont::swap().

◆ incoming_edges

template<class codeT, class guardT>
std::set<targett> goto_program_templatet< codeT, guardT >::instructiont::incoming_edges

Definition at line 207 of file goto_program_template.h.

◆ labels

template<class codeT, class guardT>
labelst goto_program_templatet< codeT, guardT >::instructiont::labels

Definition at line 204 of file goto_program_template.h.

◆ location_number

template<class codeT, class guardT>
unsigned goto_program_templatet< codeT, guardT >::instructiont::location_number

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 314 of file goto_program_template.h.

Referenced by goto_program_templatet< codeT, guardT >::instructiont::is_backwards_goto().

◆ loop_number

template<class codeT, class guardT>
unsigned goto_program_templatet< codeT, guardT >::instructiont::loop_number

Number unique per function to identify loops.

Definition at line 317 of file goto_program_template.h.

◆ nil_target

template<class codeT, class guardT>
const unsigned goto_program_templatet< codeT, guardT >::instructiont::nil_target
static
Initial value:
=
std::numeric_limits<unsigned>::max()

Uniquely identify an invalid target or location.

Definition at line 307 of file goto_program_template.h.

Referenced by goto_program_templatet< codeT, guardT >::instructiont::is_target().

◆ source_location

template<class codeT, class guardT>
source_locationt goto_program_templatet< codeT, guardT >::instructiont::source_location

The location of the instruction in the source file.

Definition at line 168 of file goto_program_template.h.

Referenced by goto_program_templatet< codeT, guardT >::instructiont::swap().

◆ target_number

template<class codeT, class guardT>
unsigned goto_program_templatet< codeT, guardT >::instructiont::target_number

A number to identify branch targets.

This is nil_target if it's not a target.

Definition at line 321 of file goto_program_template.h.

Referenced by goto_program_templatet< codeT, guardT >::instructiont::is_target().

◆ targets

template<class codeT, class guardT>
targetst goto_program_templatet< codeT, guardT >::instructiont::targets

The list of successor instructions.

Definition at line 184 of file goto_program_template.h.

Referenced by goto_program_templatet< codeT, guardT >::instructiont::clear(), goto_program_templatet< codeT, guardT >::instructiont::get_target(), goto_program_templatet< codeT, guardT >::instructiont::is_backwards_goto(), goto_program_templatet< codeT, guardT >::instructiont::make_goto(), goto_program_templatet< codeT, guardT >::instructiont::set_target(), and goto_program_templatet< codeT, guardT >::instructiont::swap().

◆ type

template<class codeT, class guardT>
goto_program_instruction_typet goto_program_templatet< codeT, guardT >::instructiont::type

What kind of instruction?

Definition at line 171 of file goto_program_template.h.

Referenced by goto_program_templatet< codeT, guardT >::instructiont::clear(), goto_program_templatet< codeT, guardT >::instructiont::is_assert(), goto_program_templatet< codeT, guardT >::instructiont::is_assign(), goto_program_templatet< codeT, guardT >::instructiont::is_assume(), goto_program_templatet< codeT, guardT >::instructiont::is_atomic_begin(), goto_program_templatet< codeT, guardT >::instructiont::is_atomic_end(), goto_program_templatet< codeT, guardT >::instructiont::is_catch(), goto_program_templatet< codeT, guardT >::instructiont::is_dead(), goto_program_templatet< codeT, guardT >::instructiont::is_decl(), goto_program_templatet< codeT, guardT >::instructiont::is_end_function(), goto_program_templatet< codeT, guardT >::instructiont::is_end_thread(), goto_program_templatet< codeT, guardT >::instructiont::is_function_call(), goto_program_templatet< codeT, guardT >::instructiont::is_goto(), goto_program_templatet< codeT, guardT >::instructiont::is_location(), goto_program_templatet< codeT, guardT >::instructiont::is_other(), goto_program_templatet< codeT, guardT >::instructiont::is_return(), goto_program_templatet< codeT, guardT >::instructiont::is_skip(), goto_program_templatet< codeT, guardT >::instructiont::is_start_thread(), goto_program_templatet< codeT, guardT >::instructiont::is_throw(), goto_program_templatet< codeT, guardT >::instructiont::swap(), and goto_program_templatet< codeT, guardT >::instructiont::to_string().

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