cprover
|
This class represents an instruction in the GOTO intermediate representation. More...
#include <goto_program_template.h>
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... | |
This class represents an instruction in the GOTO intermediate representation.
Three fields are key:
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:
guard
then goto targets
code
(which shall be either nil or an instance of code_returnt) and then jump to the end of the function.code
(an instance of code_declt), the life-time of which is bounded by a corresponding DEAD instruction.code
(an instance of code_function_callt).code
(an instance of code_assignt) to the value of the right-hand side.code
(an instance of codet of kind ID_fence, ID_printf, ID_array_copy, ID_array_set, ID_input, ID_output, ...).guard
to evaluate to true.guard
evaluates to false.exception1
, ..., exceptionN
where the list of exceptions is extracted from the code
fieldexception1
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.Definition at line 159 of file goto_program_template.h.
typedef std::list<const_targett> goto_program_templatet< codeT, guardT >::instructiont::const_targetst |
Definition at line 181 of file goto_program_template.h.
typedef std::list<instructiont>::const_iterator goto_program_templatet< codeT, guardT >::instructiont::const_targett |
Definition at line 179 of file goto_program_template.h.
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.
typedef std::list<targett> goto_program_templatet< codeT, guardT >::instructiont::targetst |
Definition at line 180 of file goto_program_template.h.
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.
|
inline |
Definition at line 273 of file goto_program_template.h.
|
inlineexplicit |
Definition at line 278 of file goto_program_template.h.
|
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().
|
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.
|
inline |
Definition at line 266 of file goto_program_template.h.
References ASSERT, and goto_program_templatet< codeT, guardT >::instructiont::type.
|
inline |
Definition at line 256 of file goto_program_template.h.
References ASSIGN, and goto_program_templatet< codeT, guardT >::instructiont::type.
|
inline |
Definition at line 265 of file goto_program_template.h.
References ASSUME, and goto_program_templatet< codeT, guardT >::instructiont::type.
|
inline |
Definition at line 267 of file goto_program_template.h.
References ATOMIC_BEGIN, and goto_program_templatet< codeT, guardT >::instructiont::type.
|
inline |
Definition at line 268 of file goto_program_template.h.
References ATOMIC_END, and goto_program_templatet< codeT, guardT >::instructiont::type.
|
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.
|
inline |
Definition at line 259 of file goto_program_template.h.
References CATCH, and goto_program_templatet< codeT, guardT >::instructiont::type.
|
inline |
Definition at line 264 of file goto_program_template.h.
References DEAD, and goto_program_templatet< codeT, guardT >::instructiont::type.
|
inline |
Definition at line 263 of file goto_program_template.h.
References DECL, and goto_program_templatet< codeT, guardT >::instructiont::type.
|
inline |
Definition at line 271 of file goto_program_template.h.
References END_FUNCTION, and goto_program_templatet< codeT, guardT >::instructiont::type.
|
inline |
Definition at line 270 of file goto_program_template.h.
References END_THREAD, and goto_program_templatet< codeT, guardT >::instructiont::type.
|
inline |
Definition at line 257 of file goto_program_template.h.
References FUNCTION_CALL, and goto_program_templatet< codeT, guardT >::instructiont::type.
|
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().
|
inline |
Definition at line 261 of file goto_program_template.h.
References LOCATION, and goto_program_templatet< codeT, guardT >::instructiont::type.
|
inline |
Definition at line 262 of file goto_program_template.h.
References OTHER, and goto_program_templatet< codeT, guardT >::instructiont::type.
|
inline |
Definition at line 255 of file goto_program_template.h.
References RETURN, and goto_program_templatet< codeT, guardT >::instructiont::type.
|
inline |
Definition at line 260 of file goto_program_template.h.
References SKIP, and goto_program_templatet< codeT, guardT >::instructiont::type.
|
inline |
Definition at line 269 of file goto_program_template.h.
References START_THREAD, and goto_program_templatet< codeT, guardT >::instructiont::type.
|
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.
|
inline |
Definition at line 258 of file goto_program_template.h.
References THROW, and goto_program_templatet< codeT, guardT >::instructiont::type.
|
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.
|
inline |
Definition at line 229 of file goto_program_template.h.
References ASSIGN, and goto_program_templatet< codeT, guardT >::instructiont::clear().
|
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.
|
inline |
Definition at line 233 of file goto_program_template.h.
References ATOMIC_BEGIN, and goto_program_templatet< codeT, guardT >::instructiont::clear().
|
inline |
Definition at line 234 of file goto_program_template.h.
References ATOMIC_END, and goto_program_templatet< codeT, guardT >::instructiont::clear().
|
inline |
Definition at line 226 of file goto_program_template.h.
References CATCH, and goto_program_templatet< codeT, guardT >::instructiont::clear().
|
inline |
Definition at line 232 of file goto_program_template.h.
References goto_program_templatet< codeT, guardT >::instructiont::clear(), and DEAD.
|
inline |
Definition at line 231 of file goto_program_template.h.
References goto_program_templatet< codeT, guardT >::instructiont::clear(), and DECL.
|
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.
|
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().
|
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.
|
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().
|
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.
|
inline |
Definition at line 223 of file goto_program_template.h.
References goto_program_templatet< codeT, guardT >::instructiont::clear(), and RETURN.
|
inline |
Definition at line 224 of file goto_program_template.h.
References goto_program_templatet< codeT, guardT >::instructiont::clear(), and SKIP.
|
inline |
Definition at line 225 of file goto_program_template.h.
References goto_program_templatet< codeT, guardT >::instructiont::clear(), and THROW.
|
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.
|
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.
|
inline |
Definition at line 336 of file goto_program_template.h.
References goto_program_templatet< codeT, guardT >::instructiont::type.
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().
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().
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().
std::set<targett> goto_program_templatet< codeT, guardT >::instructiont::incoming_edges |
Definition at line 207 of file goto_program_template.h.
labelst goto_program_templatet< codeT, guardT >::instructiont::labels |
Definition at line 204 of file goto_program_template.h.
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().
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.
|
static |
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_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().
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().
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().
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().