cprover
|
This class represents an instruction in the GOTO intermediate representation. More...
#include <goto_program.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 | |
const codet & | get_code () const |
Get the code represented by this instruction. More... | |
codet & | code_nonconst () |
Set the code represented by this instruction. More... | |
const exprt & | assign_lhs () const |
Get the lhs of the assignment for ASSIGN. More... | |
exprt & | assign_lhs_nonconst () |
Get the lhs of the assignment for ASSIGN. More... | |
const exprt & | assign_rhs () const |
Get the rhs of the assignment for ASSIGN. More... | |
exprt & | assign_rhs_nonconst () |
Get the rhs of the assignment for ASSIGN. More... | |
const symbol_exprt & | decl_symbol () const |
Get the declared symbol for DECL. More... | |
symbol_exprt & | decl_symbol () |
Get the declared symbol for DECL. More... | |
const symbol_exprt & | dead_symbol () const |
Get the symbol for DEAD. More... | |
symbol_exprt & | dead_symbol () |
Get the symbol for DEAD. More... | |
const exprt & | return_value () const |
Get the return value of a SET_RETURN_VALUE instruction. More... | |
exprt & | return_value () |
Get the return value of a SET_RETURN_VALUE instruction. More... | |
const exprt & | call_function () const |
Get the function that is called for FUNCTION_CALL. More... | |
exprt & | call_function () |
Get the function that is called for FUNCTION_CALL. More... | |
const exprt & | call_lhs () const |
Get the lhs of a FUNCTION_CALL (may be nil) More... | |
exprt & | call_lhs () |
Get the lhs of a FUNCTION_CALL (may be nil) More... | |
const exprt::operandst & | call_arguments () const |
Get the arguments of a FUNCTION_CALL. More... | |
exprt::operandst & | call_arguments () |
Get the arguments of a FUNCTION_CALL. More... | |
const codet & | get_other () const |
Get the statement for OTHER. More... | |
void | set_other (codet &c) |
Set the statement for OTHER. More... | |
const source_locationt & | source_location () const |
source_locationt & | source_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 exprt & | get_condition () const |
Get the condition of gotos, assume, assert. More... | |
void | set_condition (exprt c) |
Set the condition of gotos, assume, assert. More... | |
const exprt & | condition () const |
Get the condition of gotos, assume, assert. More... | |
exprt & | condition_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 (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... | |
Public Attributes | |
exprt | guard |
Guard for gotos, assume, assert Use condition() method to access. More... | |
targetst | targets |
The list of successor instructions. More... | |
labelst | labels |
std::set< targett > | incoming_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 | |
codet | code |
Do not read or modify directly – use get_X() instead. More... | |
source_locationt | _source_location |
The location of the instruction in the source file. More... | |
goto_program_instruction_typet | _type |
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:
targets
if and only if guard
is true. More than one target is deprecated. Its semantics was a non-deterministic choice.return_value()
. The control flow is not altered. Many analysis tools remove these instructions before they start.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.code
. After a DEAD instruction the symbol must be DECL'd again before use.call_function
with the arguments returned by call_arguments
, then assign the return value (if any) to call_lhs
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. Assume does not "retro-actively" affect the thread or any ASSERTs.guard
is true in all possible executions, otherwise it is false / unsafe. The status of the assertion does not affect execution in any way.exception1
, ..., exceptionN
where the list of exceptions is extracted from the code
field Many analysis tools remove these instructions before they start.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.Definition at line 179 of file goto_program.h.
typedef std::list<const_targett> goto_programt::instructiont::const_targetst |
Definition at line 400 of file goto_program.h.
typedef std::list<instructiont>::const_iterator goto_programt::instructiont::const_targett |
Definition at line 398 of file goto_program.h.
typedef std::list<irep_idt> goto_programt::instructiont::labelst |
Goto target labels.
Definition at line 427 of file goto_program.h.
typedef std::list<targett> goto_programt::instructiont::targetst |
Definition at line 399 of file goto_program.h.
typedef std::list<instructiont>::iterator goto_programt::instructiont::targett |
The target for gotos and for start_thread nodes.
Definition at line 397 of file goto_program.h.
|
inline |
Definition at line 493 of file goto_program.h.
|
inlineexplicit |
Definition at line 498 of file goto_program.h.
|
inline |
Constructor that can set all members, passed by value.
Definition at line 507 of file goto_program.h.
void goto_programt::instructiont::apply | ( | std::function< void(const exprt &)> | f | ) | const |
Apply given function to all expressions.
Definition at line 1059 of file goto_program.cpp.
|
inline |
Get the lhs of the assignment for ASSIGN.
Definition at line 199 of file goto_program.h.
|
inline |
Get the lhs of the assignment for ASSIGN.
Definition at line 206 of file goto_program.h.
|
inline |
Get the rhs of the assignment for ASSIGN.
Definition at line 213 of file goto_program.h.
|
inline |
Get the rhs of the assignment for ASSIGN.
Definition at line 220 of file goto_program.h.
|
inline |
Get the arguments of a FUNCTION_CALL.
Definition at line 306 of file goto_program.h.
|
inline |
Get the arguments of a FUNCTION_CALL.
Definition at line 299 of file goto_program.h.
|
inline |
Get the function that is called for FUNCTION_CALL.
Definition at line 278 of file goto_program.h.
|
inline |
Get the function that is called for FUNCTION_CALL.
Definition at line 271 of file goto_program.h.
|
inline |
Get the lhs of a FUNCTION_CALL (may be nil)
Definition at line 292 of file goto_program.h.
|
inline |
Get the lhs of a FUNCTION_CALL (may be nil)
Definition at line 285 of file goto_program.h.
|
inline |
Clear the node.
Definition at line 438 of file goto_program.h.
|
inline |
Set the code represented by this instruction.
Definition at line 193 of file goto_program.h.
|
inline |
Definition at line 463 of file goto_program.h.
|
inline |
Get the condition of gotos, assume, assert.
Definition at line 382 of file goto_program.h.
|
inline |
Get the condition of gotos, assume, assert.
Definition at line 389 of file goto_program.h.
|
inline |
Get the symbol for DEAD.
Definition at line 250 of file goto_program.h.
|
inline |
Get the symbol for DEAD.
Definition at line 243 of file goto_program.h.
|
inline |
Get the declared symbol for DECL.
Definition at line 235 of file goto_program.h.
|
inline |
Get the declared symbol for DECL.
Definition at line 227 of file goto_program.h.
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 742 of file goto_program.cpp.
|
inline |
Get the code represented by this instruction.
Definition at line 187 of file goto_program.h.
|
inline |
Get the condition of gotos, assume, assert.
Definition at line 367 of file goto_program.h.
|
inline |
Get the statement for OTHER.
Definition at line 313 of file goto_program.h.
|
inline |
Returns the first (and only) successor for the usual case of a single target.
Definition at line 407 of file goto_program.h.
|
inline |
Does this instruction have a condition?
Definition at line 360 of file goto_program.h.
|
inline |
Definition at line 421 of file goto_program.h.
|
inline |
Definition at line 484 of file goto_program.h.
|
inline |
Definition at line 474 of file goto_program.h.
|
inline |
Definition at line 483 of file goto_program.h.
|
inline |
Definition at line 485 of file goto_program.h.
|
inline |
Definition at line 486 of file goto_program.h.
|
inline |
Returns true if the instruction is a backwards branch.
Definition at line 550 of file goto_program.h.
|
inline |
Definition at line 477 of file goto_program.h.
|
inline |
Definition at line 482 of file goto_program.h.
|
inline |
Definition at line 481 of file goto_program.h.
|
inline |
Definition at line 489 of file goto_program.h.
|
inline |
Definition at line 488 of file goto_program.h.
|
inline |
Definition at line 475 of file goto_program.h.
|
inline |
Definition at line 472 of file goto_program.h.
|
inline |
Definition at line 490 of file goto_program.h.
|
inline |
Definition at line 479 of file goto_program.h.
|
inline |
Definition at line 480 of file goto_program.h.
|
inline |
Definition at line 473 of file goto_program.h.
|
inline |
Definition at line 478 of file goto_program.h.
|
inline |
Definition at line 487 of file goto_program.h.
|
inline |
Is this node a branch target?
Definition at line 434 of file goto_program.h.
|
inline |
Definition at line 476 of file goto_program.h.
|
inline |
Get the return value of a SET_RETURN_VALUE instruction.
Definition at line 264 of file goto_program.h.
|
inline |
Get the return value of a SET_RETURN_VALUE instruction.
Definition at line 257 of file goto_program.h.
|
inline |
Set the condition of gotos, assume, assert.
Definition at line 375 of file goto_program.h.
|
inline |
Set the statement for OTHER.
Definition at line 320 of file goto_program.h.
|
inline |
Sets the first (and only) successor for the usual case of a single target.
Definition at line 415 of file goto_program.h.
|
inline |
Definition at line 332 of file goto_program.h.
|
inline |
Definition at line 337 of file goto_program.h.
|
inline |
Swap two instructions.
Definition at line 522 of file goto_program.h.
|
inline |
Definition at line 562 of file goto_program.h.
Apply given transformer to all expressions; no return value means no change needed.
Definition at line 955 of file goto_program.cpp.
|
inline |
Transforms either an assertion or a GOTO instruction into an assumption, with the same condition.
Definition at line 455 of file goto_program.h.
|
inline |
Transforms an existing instruction into a skip, retaining the source_location.
Definition at line 448 of file goto_program.h.
|
inline |
What kind of instruction?
Definition at line 343 of file goto_program.h.
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 754 of file goto_program.cpp.
|
protected |
The location of the instruction in the source file.
Use source_location() to access.
Definition at line 329 of file goto_program.h.
|
protected |
Definition at line 351 of file goto_program.h.
|
protected |
Do not read or modify directly – use get_X() instead.
Definition at line 183 of file goto_program.h.
exprt goto_programt::instructiont::guard |
Guard for gotos, assume, assert Use condition() method to access.
This member will eventually be protected.
Definition at line 357 of file goto_program.h.
std::set<targett> goto_programt::instructiont::incoming_edges |
Definition at line 431 of file goto_program.h.
labelst goto_programt::instructiont::labels |
Definition at line 428 of file goto_program.h.
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 540 of file goto_program.h.
unsigned goto_programt::instructiont::loop_number = 0 |
Number unique per function to identify loops.
Definition at line 543 of file goto_program.h.
|
static |
Uniquely identify an invalid target or location.
Definition at line 534 of file goto_program.h.
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 547 of file goto_program.h.
targetst goto_programt::instructiont::targets |
The list of successor instructions.
Definition at line 403 of file goto_program.h.