cprover
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:
[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 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 make_return ()
 
void make_skip ()
 
void make_location (const source_locationt &l)
 
void make_throw ()
 
void make_catch ()
 
void make_assertion (const exprt &g)
 
void make_assumption (const exprt &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_end_function ()
 
void make_incomplete_goto (const code_gotot &_code)
 
void make_goto (targett _target)
 
void make_goto (targett _target, const exprt &g)
 
void complete_goto (targett _target)
 
void make_assignment (const codet &_code)
 
void make_decl (const codet &_code)
 
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
 
bool is_incomplete_goto () 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...
 
exprt 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

This class represents an instruction in the GOTO intermediate representation.

Three fields are key:

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

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

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

Definition at line 173 of file goto_program.h.

Member Typedef Documentation

◆ const_targetst

Definition at line 195 of file goto_program.h.

◆ const_targett

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

Definition at line 193 of file goto_program.h.

◆ labelst

Goto target labels.

Definition at line 222 of file goto_program.h.

◆ targetst

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

Constructor & Destructor Documentation

◆ instructiont() [1/2]

goto_programt::instructiont::instructiont ( )
inline

Definition at line 323 of file goto_program.h.

◆ instructiont() [2/2]

goto_programt::instructiont::instructiont ( goto_program_instruction_typet  _type)
inlineexplicit

Definition at line 328 of file goto_program.h.

Member Function Documentation

◆ clear()

◆ complete_goto()

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

Definition at line 275 of file goto_program.h.

References GOTO, INCOMPLETE_GOTO, PRECONDITION, targets, and type.

Referenced by goto_convertt::finish_gotos().

◆ get_target()

targett goto_programt::instructiont::get_target ( ) const
inline

◆ has_target()

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

Definition at line 216 of file goto_program.h.

References targets.

◆ is_assert()

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

◆ is_assign()

◆ is_assume()

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

◆ is_atomic_begin()

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

Definition at line 313 of file goto_program.h.

References ATOMIC_BEGIN, and type.

Referenced by instrumentert::cfg_visitort::visit_cfg_function().

◆ is_atomic_end()

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

Definition at line 314 of file goto_program.h.

References ATOMIC_END, and type.

Referenced by instrumentert::cfg_visitort::visit_cfg_function().

◆ is_backwards_goto()

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

Returns true if the instruction is a backwards branch.

Definition at line 374 of file goto_program.h.

References is_goto(), location_number, and targets.

Referenced by goto_symext::symex_goto(), instrumentert::cfg_visitort::visit_cfg_goto(), and dott::write_edge().

◆ is_catch()

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

Definition at line 305 of file goto_program.h.

References CATCH, and type.

◆ is_dead()

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

Definition at line 310 of file goto_program.h.

References DEAD, and type.

Referenced by goto_checkt::goto_check().

◆ is_decl()

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

Definition at line 309 of file goto_program.h.

References DECL, and type.

Referenced by uninitializedt::add_assertions().

◆ is_end_function()

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

Definition at line 317 of file goto_program.h.

References END_FUNCTION, and type.

Referenced by goto_checkt::goto_check(), and goto_inlinet::insert_function_body().

◆ is_end_thread()

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

◆ is_function_call()

◆ is_goto()

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

◆ is_incomplete_goto()

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

Definition at line 318 of file goto_program.h.

References INCOMPLETE_GOTO, and type.

◆ is_location()

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

Definition at line 307 of file goto_program.h.

References LOCATION, and type.

◆ is_other()

◆ is_return()

◆ is_skip()

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

Definition at line 306 of file goto_program.h.

References SKIP, and type.

◆ is_start_thread()

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

◆ is_target()

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

Is this node a branch target?

Definition at line 229 of file goto_program.h.

References nil_target, and target_number.

Referenced by goto_checkt::goto_check(), goto_programt::output_instruction(), and read_bin_goto_object_v3().

◆ is_throw()

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

Definition at line 304 of file goto_program.h.

References THROW, and type.

Referenced by goto_programt::get_successors(), and goto_checkt::goto_check().

◆ make_assertion()

void goto_programt::instructiont::make_assertion ( const exprt g)
inline

Definition at line 247 of file goto_program.h.

References ASSERT, clear(), and guard.

◆ make_assignment() [1/2]

void goto_programt::instructiont::make_assignment ( )
inline

◆ make_assignment() [2/2]

void goto_programt::instructiont::make_assignment ( const codet _code)
inline

Definition at line 282 of file goto_program.h.

References ASSIGN, clear(), and code.

◆ make_assumption()

void goto_programt::instructiont::make_assumption ( const exprt g)
inline

Definition at line 248 of file goto_program.h.

References ASSUME, clear(), and guard.

Referenced by undefined_function_abort_path().

◆ make_atomic_begin()

void goto_programt::instructiont::make_atomic_begin ( )
inline

◆ make_atomic_end()

void goto_programt::instructiont::make_atomic_end ( )
inline

Definition at line 254 of file goto_program.h.

References ATOMIC_END, and clear().

◆ make_catch()

void goto_programt::instructiont::make_catch ( )
inline

Definition at line 246 of file goto_program.h.

References CATCH, and clear().

◆ make_dead()

void goto_programt::instructiont::make_dead ( )
inline

Definition at line 252 of file goto_program.h.

References clear(), and DEAD.

◆ make_decl() [1/2]

void goto_programt::instructiont::make_decl ( )
inline

Definition at line 251 of file goto_program.h.

References clear(), and DECL.

Referenced by insert_nondet_init_code().

◆ make_decl() [2/2]

void goto_programt::instructiont::make_decl ( const codet _code)
inline

Definition at line 288 of file goto_program.h.

References clear(), code, and DECL.

◆ make_end_function()

void goto_programt::instructiont::make_end_function ( )
inline

Definition at line 255 of file goto_program.h.

References clear(), and END_FUNCTION.

◆ make_function_call()

void goto_programt::instructiont::make_function_call ( const codet _code)
inline

Definition at line 294 of file goto_program.h.

References clear(), code, and FUNCTION_CALL.

Referenced by function_exit().

◆ make_goto() [1/2]

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

Definition at line 263 of file goto_program.h.

References clear(), GOTO, and targets.

Referenced by make_goto().

◆ make_goto() [2/2]

void goto_programt::instructiont::make_goto ( targett  _target,
const exprt g 
)
inline

Definition at line 269 of file goto_program.h.

References guard, and make_goto().

◆ make_incomplete_goto()

void goto_programt::instructiont::make_incomplete_goto ( const code_gotot _code)
inline

Definition at line 257 of file goto_program.h.

References clear(), code, and INCOMPLETE_GOTO.

◆ make_location()

void goto_programt::instructiont::make_location ( const source_locationt l)
inline

Definition at line 243 of file goto_program.h.

References clear(), LOCATION, and source_location.

◆ make_other()

void goto_programt::instructiont::make_other ( const codet _code)
inline

Definition at line 250 of file goto_program.h.

References clear(), code, and OTHER.

◆ make_return()

void goto_programt::instructiont::make_return ( )
inline

Definition at line 241 of file goto_program.h.

References clear(), and RETURN.

◆ make_skip()

void goto_programt::instructiont::make_skip ( )
inline

Definition at line 242 of file goto_program.h.

References clear(), and SKIP.

Referenced by check_and_replace_target(), goto_checkt::goto_check(), and race_check().

◆ make_throw()

void goto_programt::instructiont::make_throw ( )
inline

Definition at line 245 of file goto_program.h.

References clear(), and THROW.

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

References targets.

◆ swap()

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

◆ to_string()

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

Definition at line 386 of file goto_program.h.

References type.

Referenced by show_goto_functions_jsont::convert(), and show_goto_functions_xmlt::convert().

Member Data Documentation

◆ code

codet goto_programt::instructiont::code

Definition at line 176 of file goto_program.h.

Referenced by string_abstractiont::abstract_pointer_assign(), overflow_instrumentert::accumulate_overflow(), uninitializedt::add_assertions(), acceleratet::add_dirty_checks(), as_string(), local_may_aliast::build(), local_bitvector_analysist::build(), clear(), goto_checkt::collect_allocations(), cfg_baset< cfg_nodet >::compute_edges_function_call(), procedure_local_cfg_baset< nodet, goto_programt, goto_programt::targett >::compute_edges_function_call(), cone_of_influencet::cone_of_influence(), show_goto_functions_jsont::convert(), show_goto_functions_xmlt::convert(), goto_program_dereferencet::dereference_instruction(), expressions_read(), expressions_written(), goto_convertt::finish_computed_gotos(), goto_convertt::finish_gotos(), get_modifies(), function_modifiest::get_modifies(), havoc_loopst::get_modifies(), goto_checkt::goto_check(), unified_difft::instructions_equal(), taint_analysist::instrument(), escape_analysist::instrument(), introduce_temporaries(), is_assignment_from(), is_fence(), is_lwfence(), is_return_with_variable(), make_assignment(), make_decl(), make_function_call(), make_incomplete_goto(), make_other(), mmio(), nondet_static(), nondet_volatile(), does_remove_constt::operator()(), replace_callst::operator()(), goto_programt::output_instruction(), remove_asmt::process_instruction(), read_bin_goto_object_v3(), goto_symext::return_assignment(), swap(), goto_symext::symex_catch(), goto_symext::symex_dead(), goto_symext::symex_decl(), goto_symext::symex_goto(), goto_symext::symex_other(), goto_symext::symex_throw(), uncaught_exceptions_domaint::transform(), custom_bitvector_domaint::transform(), global_may_alias_domaint::transform(), escape_domaint::transform(), interval_domaint::transform(), undefined_function_abort_path(), instrumentert::cfg_visitort::visit_cfg_asm_fence(), instrumentert::cfg_visitort::visit_cfg_function(), instrumentert::cfg_visitort::visit_cfg_function_call(), shared_bufferst::cfg_visitort::weak_memory(), shared_bufferst::write(), and write_goto_binary_v3().

◆ function

◆ guard

◆ incoming_edges

◆ labels

◆ location_number

unsigned goto_programt::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 364 of file goto_program.h.

Referenced by is_backwards_goto(), goto_programt::output_instruction(), and dott::write_edge().

◆ loop_number

unsigned goto_programt::instructiont::loop_number

Number unique per function to identify loops.

Definition at line 367 of file goto_program.h.

Referenced by goto_programt::loop_id().

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

Referenced by goto_inlinet::check_inline_map(), goto_programt::compute_target_numbers(), is_target(), and goto_convertt::optimize_guarded_gotos().

◆ source_location

◆ target_number

unsigned goto_programt::instructiont::target_number

A number to identify branch targets.

This is nil_target if it's not a target.

Definition at line 371 of file goto_program.h.

Referenced by is_target(), goto_programt::output_instruction(), read_bin_goto_object_v3(), and write_goto_binary_v3().

◆ targets

◆ type


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