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 code_assignt & | get_assign () const |
Get the assignment for ASSIGN. 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... | |
void | set_assign (code_assignt c) |
Set the assignment for ASSIGN. More... | |
const code_declt & | get_decl () const |
Get the declaration for DECL. 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... | |
void | set_decl (code_declt c) |
Set the declaration for DECL. More... | |
const code_deadt & | get_dead () const |
Get the dead statement for DEAD. More... | |
const symbol_exprt & | dead_symbol () const |
Get the symbol for DEAD. More... | |
symbol_exprt & | dead_symbol () |
Get the symbol for DEAD. More... | |
void | set_dead (code_deadt c) |
Set the dead statement for DEAD. More... | |
const code_returnt & | get_return () const |
Get the return statement for READ. 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... | |
void | set_return (code_returnt c) |
Set the return statement for SET_RETURN_VALUE. More... | |
const code_function_callt & | get_function_call () const |
Get the function call for FUNCTION_CALL. 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... | |
void | set_function_call (code_function_callt c) |
Set the function call for 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... | |
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... | |
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 | 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 | |
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 Use get_condition() to read, and set_condition(c) to write. 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... | |
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 177 of file goto_program.h.
typedef std::list<const_targett> goto_programt::instructiont::const_targetst |
Definition at line 465 of file goto_program.h.
typedef std::list<instructiont>::const_iterator goto_programt::instructiont::const_targett |
Definition at line 463 of file goto_program.h.
typedef std::list<irep_idt> goto_programt::instructiont::labelst |
Goto target labels.
Definition at line 492 of file goto_program.h.
typedef std::list<targett> goto_programt::instructiont::targetst |
Definition at line 464 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 462 of file goto_program.h.
|
inline |
Definition at line 548 of file goto_program.h.
|
inlineexplicit |
Definition at line 553 of file goto_program.h.
|
inline |
Constructor that can set all members, passed by value.
Definition at line 562 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 1049 of file goto_program.cpp.
|
inline |
Get the lhs of the assignment for ASSIGN.
Definition at line 205 of file goto_program.h.
|
inline |
Get the lhs of the assignment for ASSIGN.
Definition at line 212 of file goto_program.h.
|
inline |
Get the rhs of the assignment for ASSIGN.
Definition at line 219 of file goto_program.h.
|
inline |
Get the rhs of the assignment for ASSIGN.
Definition at line 226 of file goto_program.h.
|
inline |
Get the arguments of a FUNCTION_CALL.
Definition at line 396 of file goto_program.h.
|
inline |
Get the arguments of a FUNCTION_CALL.
Definition at line 389 of file goto_program.h.
|
inline |
Get the function that is called for FUNCTION_CALL.
Definition at line 368 of file goto_program.h.
|
inline |
Get the function that is called for FUNCTION_CALL.
Definition at line 361 of file goto_program.h.
|
inline |
Get the lhs of a FUNCTION_CALL (may be nil)
Definition at line 382 of file goto_program.h.
|
inline |
Get the lhs of a FUNCTION_CALL (may be nil)
Definition at line 375 of file goto_program.h.
|
inline |
Clear the node.
Definition at line 503 of file goto_program.h.
|
inline |
Set the code represented by this instruction.
Definition at line 191 of file goto_program.h.
|
inline |
Definition at line 518 of file goto_program.h.
|
inline |
Get the symbol for DEAD.
Definition at line 302 of file goto_program.h.
|
inline |
Get the symbol for DEAD.
Definition at line 295 of file goto_program.h.
|
inline |
Get the declared symbol for DECL.
Definition at line 264 of file goto_program.h.
|
inline |
Get the declared symbol for DECL.
Definition at line 253 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 732 of file goto_program.cpp.
|
inline |
Get the assignment for ASSIGN.
Definition at line 198 of file goto_program.h.
|
inline |
Get the code represented by this instruction.
Definition at line 185 of file goto_program.h.
|
inline |
Get the condition of gotos, assume, assert.
Definition at line 447 of file goto_program.h.
|
inline |
Get the dead statement for DEAD.
Definition at line 288 of file goto_program.h.
|
inline |
Get the declaration for DECL.
Definition at line 242 of file goto_program.h.
|
inline |
Get the function call for FUNCTION_CALL.
Definition at line 353 of file goto_program.h.
|
inline |
Get the statement for OTHER.
Definition at line 417 of file goto_program.h.
|
inline |
Get the return statement for READ.
Definition at line 318 of file goto_program.h.
|
inline |
Returns the first (and only) successor for the usual case of a single target.
Definition at line 472 of file goto_program.h.
|
inline |
Does this instruction have a condition?
Definition at line 441 of file goto_program.h.
|
inline |
Definition at line 486 of file goto_program.h.
|
inline |
Definition at line 539 of file goto_program.h.
|
inline |
Definition at line 529 of file goto_program.h.
|
inline |
Definition at line 538 of file goto_program.h.
|
inline |
Definition at line 540 of file goto_program.h.
|
inline |
Definition at line 541 of file goto_program.h.
|
inline |
Returns true if the instruction is a backwards branch.
Definition at line 604 of file goto_program.h.
|
inline |
Definition at line 532 of file goto_program.h.
|
inline |
Definition at line 537 of file goto_program.h.
|
inline |
Definition at line 536 of file goto_program.h.
|
inline |
Definition at line 544 of file goto_program.h.
|
inline |
Definition at line 543 of file goto_program.h.
|
inline |
Definition at line 530 of file goto_program.h.
|
inline |
Definition at line 527 of file goto_program.h.
|
inline |
Definition at line 545 of file goto_program.h.
|
inline |
Definition at line 534 of file goto_program.h.
|
inline |
Definition at line 535 of file goto_program.h.
|
inline |
Definition at line 528 of file goto_program.h.
|
inline |
Definition at line 533 of file goto_program.h.
|
inline |
Definition at line 542 of file goto_program.h.
|
inline |
Is this node a branch target?
Definition at line 499 of file goto_program.h.
|
inline |
Definition at line 531 of file goto_program.h.
|
inline |
Get the return value of a SET_RETURN_VALUE instruction.
Definition at line 332 of file goto_program.h.
|
inline |
Get the return value of a SET_RETURN_VALUE instruction.
Definition at line 325 of file goto_program.h.
|
inline |
Set the assignment for ASSIGN.
Definition at line 234 of file goto_program.h.
|
inline |
Set the condition of gotos, assume, assert.
Definition at line 454 of file goto_program.h.
|
inline |
Set the dead statement for DEAD.
Definition at line 310 of file goto_program.h.
|
inline |
Set the declaration for DECL.
Definition at line 276 of file goto_program.h.
|
inline |
Set the function call for FUNCTION_CALL.
Definition at line 409 of file goto_program.h.
|
inline |
Set the statement for OTHER.
Definition at line 424 of file goto_program.h.
|
inline |
Set the return statement for SET_RETURN_VALUE.
Definition at line 340 of file goto_program.h.
|
inline |
Sets the first (and only) successor for the usual case of a single target.
Definition at line 480 of file goto_program.h.
|
inline |
Swap two instructions.
Definition at line 577 of file goto_program.h.
|
inline |
Definition at line 616 of file goto_program.h.
Apply given transformer to all expressions; no return value means no change needed.
Definition at line 945 of file goto_program.cpp.
|
inline |
Transforms an existing instruction into a skip, retaining the source_location.
Definition at line 513 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 744 of file goto_program.cpp.
|
protected |
Do not read or modify directly – use get_X() instead.
Definition at line 181 of file goto_program.h.
exprt goto_programt::instructiont::guard |
Guard for gotos, assume, assert Use get_condition() to read, and set_condition(c) to write.
Definition at line 438 of file goto_program.h.
std::set<targett> goto_programt::instructiont::incoming_edges |
Definition at line 496 of file goto_program.h.
labelst goto_programt::instructiont::labels |
Definition at line 493 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 594 of file goto_program.h.
unsigned goto_programt::instructiont::loop_number = 0 |
Number unique per function to identify loops.
Definition at line 597 of file goto_program.h.
|
static |
Uniquely identify an invalid target or location.
Definition at line 588 of file goto_program.h.
source_locationt goto_programt::instructiont::source_location |
The location of the instruction in the source file.
Definition at line 431 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 601 of file goto_program.h.
targetst goto_programt::instructiont::targets |
The list of successor instructions.
Definition at line 468 of file goto_program.h.
goto_program_instruction_typet goto_programt::instructiont::type |
What kind of instruction?
Definition at line 434 of file goto_program.h.