CBMC
|
This class represents an instruction in the GOTO intermediate representation. More...
#include <goto_program.h>
Classes | |
struct | target_less_than |
A total order over targett and const_targett . More... | |
Public Types | |
typedef std::list< instructiont >::iterator | targett |
The target for gotos and for start_thread nodes. | |
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. | |
Public Member Functions | |
const goto_instruction_codet & | code () const |
Get the code represented by this instruction. | |
goto_instruction_codet & | code_nonconst () |
Set the code represented by this instruction. | |
const exprt & | assign_lhs () const |
Get the lhs of the assignment for ASSIGN. | |
exprt & | assign_lhs_nonconst () |
Get the lhs of the assignment for ASSIGN. | |
const exprt & | assign_rhs () const |
Get the rhs of the assignment for ASSIGN. | |
exprt & | assign_rhs_nonconst () |
Get the rhs of the assignment for ASSIGN. | |
const symbol_exprt & | decl_symbol () const |
Get the declared symbol for DECL. | |
symbol_exprt & | decl_symbol () |
Get the declared symbol for DECL. | |
const symbol_exprt & | dead_symbol () const |
Get the symbol for DEAD. | |
symbol_exprt & | dead_symbol () |
Get the symbol for DEAD. | |
const exprt & | return_value () const |
Get the return value of a SET_RETURN_VALUE instruction. | |
exprt & | return_value () |
Get the return value of a SET_RETURN_VALUE instruction. | |
const exprt & | call_function () const |
Get the function that is called for FUNCTION_CALL. | |
exprt & | call_function () |
Get the function that is called for FUNCTION_CALL. | |
const exprt & | call_lhs () const |
Get the lhs of a FUNCTION_CALL (may be nil) | |
exprt & | call_lhs () |
Get the lhs of a FUNCTION_CALL (may be nil) | |
const exprt::operandst & | call_arguments () const |
Get the arguments of a FUNCTION_CALL. | |
exprt::operandst & | call_arguments () |
Get the arguments of a FUNCTION_CALL. | |
const goto_instruction_codet & | get_other () const |
Get the statement for OTHER. | |
void | set_other (goto_instruction_codet &c) |
Set the statement for OTHER. | |
const source_locationt & | source_location () const |
source_locationt & | source_location_nonconst () |
goto_program_instruction_typet | type () const |
What kind of instruction? | |
bool | has_condition () const |
Does this instruction have a condition? | |
const exprt & | condition () const |
Get the condition of gotos, assume, assert. | |
exprt & | condition_nonconst () |
Get the condition of gotos, assume, assert. | |
const_targett | get_target () const |
Returns the first (and only) successor for the usual case of a single target. | |
targett | get_target () |
Returns the first (and only) successor for the usual case of a single target. | |
void | set_target (targett t) |
Sets the first (and only) successor for the usual case of a single target. | |
bool | has_target () const |
bool | is_target () const |
Is this node a branch target? | |
void | clear (goto_program_instruction_typet __type) |
Clear the node. | |
void | turn_into_skip () |
Transforms an existing instruction into a skip, retaining the source_location. | |
void | turn_into_assume () |
Transforms either an assertion or a GOTO instruction into an assumption, with the same condition. | |
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 (goto_instruction_codet __code, source_locationt __source_location, goto_program_instruction_typet __type, exprt _guard, targetst _targets) | |
Constructor that can set all members, passed by value. | |
void | swap (instructiont &instruction) |
Swap two instructions. | |
bool | is_backwards_goto () const |
Returns true if the instruction is a backwards branch. | |
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. | |
void | validate (const namespacet &ns, const validation_modet vm) const |
Check that the instruction is well-formed. | |
void | transform (std::function< std::optional< exprt >(exprt)>) |
Apply given transformer to all expressions; no return value means no change needed. | |
void | apply (std::function< void(const exprt &)>) const |
Apply given function to all expressions. | |
std::ostream & | output (std::ostream &) const |
Output this instruction to the given stream. | |
Public Attributes | |
targetst | targets |
The list of successor instructions. | |
labelst | labels |
std::set< targett, target_less_than > | incoming_edges |
unsigned | location_number = 0 |
A globally unique number to identify a program location. | |
unsigned | loop_number = 0 |
Number unique per function to identify loops. | |
unsigned | target_number = nil_target |
A number to identify branch targets. | |
Static Public Attributes | |
static const unsigned | nil_target |
Uniquely identify an invalid target or location. | |
Protected Attributes | |
goto_instruction_codet | _code |
Do not read or modify directly – use code() and code_nonconst() instead. | |
source_locationt | _source_location |
The location of the instruction in the source file. | |
goto_program_instruction_typet | _type |
exprt | guard |
Guard for gotos, assume, assert Use condition() method to access. | |
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 goto_instruction_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.
Definition at line 383 of file goto_program.h.
typedef std::list<instructiont>::const_iterator goto_programt::instructiont::const_targett |
Definition at line 381 of file goto_program.h.
typedef std::list<irep_idt> goto_programt::instructiont::labelst |
Goto target labels.
Definition at line 445 of file goto_program.h.
typedef std::list<targett> goto_programt::instructiont::targetst |
Definition at line 382 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 380 of file goto_program.h.
|
inline |
Definition at line 511 of file goto_program.h.
|
inlineexplicit |
Definition at line 516 of file goto_program.h.
|
inline |
Constructor that can set all members, passed by value.
Definition at line 525 of file goto_program.h.
Apply given function to all expressions.
Definition at line 1088 of file goto_program.cpp.
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.
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.
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.
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 456 of file goto_program.h.
|
inline |
Get the code represented by this instruction.
Definition at line 187 of file goto_program.h.
|
inline |
Set the code represented by this instruction.
Definition at line 193 of file goto_program.h.
Definition at line 481 of file goto_program.h.
Get the condition of gotos, assume, assert.
Definition at line 365 of file goto_program.h.
|
inline |
Get the condition of gotos, assume, assert.
Definition at line 372 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 772 of file goto_program.cpp.
|
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 425 of file goto_program.h.
|
inline |
Returns the first (and only) successor for the usual case of a single target.
Definition at line 417 of file goto_program.h.
|
inline |
Does this instruction have a condition?
Definition at line 359 of file goto_program.h.
|
inline |
Definition at line 439 of file goto_program.h.
|
inline |
Definition at line 502 of file goto_program.h.
|
inline |
Definition at line 492 of file goto_program.h.
|
inline |
Definition at line 501 of file goto_program.h.
|
inline |
Definition at line 503 of file goto_program.h.
|
inline |
Definition at line 504 of file goto_program.h.
|
inline |
Returns true if the instruction is a backwards branch.
Definition at line 568 of file goto_program.h.
|
inline |
Definition at line 495 of file goto_program.h.
|
inline |
Definition at line 500 of file goto_program.h.
|
inline |
Definition at line 499 of file goto_program.h.
|
inline |
Definition at line 507 of file goto_program.h.
|
inline |
Definition at line 506 of file goto_program.h.
|
inline |
Definition at line 493 of file goto_program.h.
|
inline |
Definition at line 490 of file goto_program.h.
|
inline |
Definition at line 508 of file goto_program.h.
|
inline |
Definition at line 497 of file goto_program.h.
|
inline |
Definition at line 498 of file goto_program.h.
|
inline |
Definition at line 491 of file goto_program.h.
|
inline |
Definition at line 496 of file goto_program.h.
|
inline |
Definition at line 505 of file goto_program.h.
|
inline |
Is this node a branch target?
Definition at line 452 of file goto_program.h.
|
inline |
Definition at line 494 of file goto_program.h.
std::ostream & goto_programt::instructiont::output | ( | std::ostream & | out | ) | const |
Output this instruction to the given stream.
Writes to out
a two/three line string representation of a given instruction
.
The output is of the format:
out | the stream to write the goto string to |
Definition at line 49 of file goto_program.cpp.
|
inline |
Get the return value of a SET_RETURN_VALUE instruction.
Definition at line 264 of file goto_program.h.
Get the return value of a SET_RETURN_VALUE instruction.
Definition at line 257 of file goto_program.h.
|
inline |
Set the statement for OTHER.
Definition at line 320 of file goto_program.h.
Sets the first (and only) successor for the usual case of a single target.
Definition at line 433 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 540 of file goto_program.h.
|
inline |
Definition at line 580 of file goto_program.h.
Apply given transformer to all expressions; no return value means no change needed.
Definition at line 984 of file goto_program.cpp.
|
inline |
Transforms either an assertion or a GOTO instruction into an assumption, with the same condition.
Definition at line 473 of file goto_program.h.
|
inline |
Transforms an existing instruction into a skip, retaining the source_location.
Definition at line 466 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 784 of file goto_program.cpp.
|
protected |
Do not read or modify directly – use code() and code_nonconst() instead.
Definition at line 183 of file goto_program.h.
|
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 |
Guard for gotos, assume, assert Use condition() method to access.
Definition at line 355 of file goto_program.h.
std::set<targett, target_less_than> goto_programt::instructiont::incoming_edges |
Definition at line 449 of file goto_program.h.
labelst goto_programt::instructiont::labels |
Definition at line 446 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 558 of file goto_program.h.
unsigned goto_programt::instructiont::loop_number = 0 |
Number unique per function to identify loops.
Definition at line 561 of file goto_program.h.
Uniquely identify an invalid target or location.
Definition at line 552 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 565 of file goto_program.h.
targetst goto_programt::instructiont::targets |
The list of successor instructions.
Definition at line 413 of file goto_program.h.