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 code_assignt & | get_assign () const |
Get 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... | |
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... | |
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... | |
void | set_return (code_returnt c) |
Set the return statement for READ. More... | |
const code_function_callt & | get_function_call () const |
Get the function call for 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 | 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 code_assignt &_code) |
void | make_decl (const code_declt &_code) |
void | make_function_call (const code_function_callt &_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) | |
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 | |
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 |
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... | |
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.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.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.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. 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 178 of file goto_program.h.
typedef std::list<const_targett> goto_programt::instructiont::const_targetst |
Definition at line 303 of file goto_program.h.
typedef std::list<instructiont>::const_iterator goto_programt::instructiont::const_targett |
Definition at line 301 of file goto_program.h.
typedef std::list<irep_idt> goto_programt::instructiont::labelst |
Goto target labels.
Definition at line 330 of file goto_program.h.
typedef std::list<targett> goto_programt::instructiont::targetst |
Definition at line 302 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 300 of file goto_program.h.
|
inline |
Definition at line 481 of file goto_program.h.
|
inlineexplicit |
Definition at line 486 of file goto_program.h.
|
inline |
Constructor that can set all members, passed by value.
Definition at line 495 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 1028 of file goto_program.cpp.
|
inline |
Clear the node.
Definition at line 341 of file goto_program.h.
|
inline |
Definition at line 427 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 697 of file goto_program.cpp.
|
inline |
Get the assignment for ASSIGN.
Definition at line 185 of file goto_program.h.
|
inline |
Get the condition of gotos, assume, assert.
Definition at line 285 of file goto_program.h.
|
inline |
Get the dead statement for DEAD.
Definition at line 213 of file goto_program.h.
|
inline |
Get the declaration for DECL.
Definition at line 199 of file goto_program.h.
|
inline |
Get the function call for FUNCTION_CALL.
Definition at line 241 of file goto_program.h.
|
inline |
Get the statement for OTHER.
Definition at line 255 of file goto_program.h.
|
inline |
Get the return statement for READ.
Definition at line 227 of file goto_program.h.
|
inline |
Returns the first (and only) successor for the usual case of a single target.
Definition at line 310 of file goto_program.h.
|
inline |
Does this instruction have a condition?
Definition at line 279 of file goto_program.h.
|
inline |
Definition at line 324 of file goto_program.h.
|
inline |
Definition at line 470 of file goto_program.h.
|
inline |
Definition at line 460 of file goto_program.h.
|
inline |
Definition at line 469 of file goto_program.h.
|
inline |
Definition at line 471 of file goto_program.h.
|
inline |
Definition at line 472 of file goto_program.h.
|
inline |
Returns true if the instruction is a backwards branch.
Definition at line 537 of file goto_program.h.
|
inline |
Definition at line 463 of file goto_program.h.
|
inline |
Definition at line 468 of file goto_program.h.
|
inline |
Definition at line 467 of file goto_program.h.
|
inline |
Definition at line 475 of file goto_program.h.
|
inline |
Definition at line 474 of file goto_program.h.
|
inline |
Definition at line 461 of file goto_program.h.
|
inline |
Definition at line 458 of file goto_program.h.
|
inline |
Definition at line 476 of file goto_program.h.
|
inline |
Definition at line 465 of file goto_program.h.
|
inline |
Definition at line 466 of file goto_program.h.
|
inline |
Definition at line 459 of file goto_program.h.
|
inline |
Definition at line 464 of file goto_program.h.
|
inline |
Definition at line 473 of file goto_program.h.
|
inline |
Is this node a branch target?
Definition at line 337 of file goto_program.h.
|
inline |
Definition at line 462 of file goto_program.h.
|
inline |
Definition at line 374 of file goto_program.h.
|
inline |
Definition at line 382 of file goto_program.h.
|
inline |
Definition at line 437 of file goto_program.h.
|
inline |
Definition at line 378 of file goto_program.h.
|
inline |
Definition at line 395 of file goto_program.h.
|
inline |
Definition at line 399 of file goto_program.h.
|
inline |
Definition at line 370 of file goto_program.h.
|
inline |
Definition at line 391 of file goto_program.h.
|
inline |
Definition at line 388 of file goto_program.h.
|
inline |
Definition at line 444 of file goto_program.h.
|
inline |
Definition at line 403 of file goto_program.h.
|
inline |
Definition at line 452 of file goto_program.h.
|
inline |
Definition at line 414 of file goto_program.h.
Definition at line 421 of file goto_program.h.
|
inline |
Definition at line 407 of file goto_program.h.
|
inline |
Definition at line 363 of file goto_program.h.
|
inline |
Definition at line 385 of file goto_program.h.
|
inline |
Definition at line 357 of file goto_program.h.
|
inline |
Definition at line 360 of file goto_program.h.
|
inline |
Definition at line 367 of file goto_program.h.
|
inline |
Set the assignment for ASSIGN.
Definition at line 192 of file goto_program.h.
|
inline |
Set the condition of gotos, assume, assert.
Definition at line 292 of file goto_program.h.
|
inline |
Set the dead statement for DEAD.
Definition at line 220 of file goto_program.h.
|
inline |
Set the declaration for DECL.
Definition at line 206 of file goto_program.h.
|
inline |
Set the function call for FUNCTION_CALL.
Definition at line 248 of file goto_program.h.
|
inline |
Set the statement for OTHER.
Definition at line 262 of file goto_program.h.
|
inline |
Set the return statement for READ.
Definition at line 234 of file goto_program.h.
|
inline |
Sets the first (and only) successor for the usual case of a single target.
Definition at line 318 of file goto_program.h.
|
inline |
Swap two instructions.
Definition at line 510 of file goto_program.h.
|
inline |
Definition at line 549 of file goto_program.h.
Apply given transformer to all expressions; no return value means no change needed.
Definition at line 910 of file goto_program.cpp.
|
inline |
Transforms an existing instruction into a skip, retaining the source_location.
Definition at line 351 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 709 of file goto_program.cpp.
codet goto_programt::instructiont::code |
Do not read or modify directly – use get_X() instead.
Definition at line 182 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 276 of file goto_program.h.
std::set<targett> goto_programt::instructiont::incoming_edges |
Definition at line 334 of file goto_program.h.
labelst goto_programt::instructiont::labels |
Definition at line 331 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 527 of file goto_program.h.
unsigned goto_programt::instructiont::loop_number = 0 |
Number unique per function to identify loops.
Definition at line 530 of file goto_program.h.
|
static |
Uniquely identify an invalid target or location.
Definition at line 521 of file goto_program.h.
source_locationt goto_programt::instructiont::source_location |
The location of the instruction in the source file.
Definition at line 269 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 534 of file goto_program.h.
targetst goto_programt::instructiont::targets |
The list of successor instructions.
Definition at line 306 of file goto_program.h.
goto_program_instruction_typet goto_programt::instructiont::type |
What kind of instruction?
Definition at line 272 of file goto_program.h.