cprover
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< targetttargetst
 
typedef std::list< const_targettconst_targetst
 
typedef std::list< irep_idtlabelst
 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< targettincoming_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]

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

§ 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.

§ 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.

§ 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.

§ 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.

Referenced by goto_programt::output_instruction().

§ 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.

§ 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.

§ 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().

§ 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.

§ 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.

§ 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.

§ 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.

§ 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.

§ 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.

§ is_goto()

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

§ 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.

§ 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.

§ 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.

§ 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.

§ 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.

§ is_target()

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

§ 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.

§ make_assertion()

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

§ make_assignment()

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

§ make_assumption()

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

§ make_atomic_begin()

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

§ make_atomic_end()

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

§ make_catch()

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

§ make_dead()

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

§ make_decl()

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

§ make_function_call()

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

§ make_goto() [1/3]

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

§ make_goto() [2/3]

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

§ make_goto() [3/3]

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

§ make_other()

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

§ make_return()

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

§ make_skip()

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

§ make_throw()

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

§ 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.

§ swap()

§ to_string()

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

Member Data Documentation

§ code

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

§ 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_programt::output_instruction(), 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.

Referenced by goto_programt::output_instruction().

§ 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_programt::output_instruction().

§ 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, exprt >::compute_target_numbers(), goto_program_templatet< codeT, guardT >::instructiont::is_target(), and goto_program_templatet< codeT, guardT >::instructiont::swap().

§ 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_programt::output_instruction(), and 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(), and goto_programt::output_instruction().

§ 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_programt::output_instruction(), and goto_program_templatet< codeT, guardT >::instructiont::swap().

§ type


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