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... | |
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 RETURN instruction. More... | |
exprt & | return_value () |
Get the return value of a RETURN instruction. 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 | complete_goto (targett _target) |
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 179 of file goto_program.h.
typedef std::list<const_targett> goto_programt::instructiont::const_targetst |
Definition at line 368 of file goto_program.h.
typedef std::list<instructiont>::const_iterator goto_programt::instructiont::const_targett |
Definition at line 366 of file goto_program.h.
typedef std::list<irep_idt> goto_programt::instructiont::labelst |
Goto target labels.
Definition at line 395 of file goto_program.h.
typedef std::list<targett> goto_programt::instructiont::targetst |
Definition at line 367 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 365 of file goto_program.h.
|
inline |
Definition at line 452 of file goto_program.h.
|
inlineexplicit |
Definition at line 457 of file goto_program.h.
|
inline |
Constructor that can set all members, passed by value.
Definition at line 466 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 1015 of file goto_program.cpp.
|
inline |
Clear the node.
Definition at line 406 of file goto_program.h.
|
inline |
Definition at line 421 of file goto_program.h.
|
inline |
Get the symbol for DEAD.
Definition at line 261 of file goto_program.h.
|
inline |
Get the symbol for DEAD.
Definition at line 254 of file goto_program.h.
|
inline |
Get the declared symbol for DECL.
Definition at line 223 of file goto_program.h.
|
inline |
Get the declared symbol for DECL.
Definition at line 212 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 696 of file goto_program.cpp.
|
inline |
Get the assignment for ASSIGN.
Definition at line 186 of file goto_program.h.
|
inline |
Get the condition of gotos, assume, assert.
Definition at line 350 of file goto_program.h.
|
inline |
Get the dead statement for DEAD.
Definition at line 247 of file goto_program.h.
|
inline |
Get the declaration for DECL.
Definition at line 201 of file goto_program.h.
|
inline |
Get the function call for FUNCTION_CALL.
Definition at line 306 of file goto_program.h.
|
inline |
Get the statement for OTHER.
Definition at line 320 of file goto_program.h.
|
inline |
Get the return statement for READ.
Definition at line 277 of file goto_program.h.
|
inline |
Returns the first (and only) successor for the usual case of a single target.
Definition at line 375 of file goto_program.h.
|
inline |
Does this instruction have a condition?
Definition at line 344 of file goto_program.h.
|
inline |
Definition at line 389 of file goto_program.h.
|
inline |
Definition at line 441 of file goto_program.h.
|
inline |
Definition at line 431 of file goto_program.h.
|
inline |
Definition at line 440 of file goto_program.h.
|
inline |
Definition at line 442 of file goto_program.h.
|
inline |
Definition at line 443 of file goto_program.h.
|
inline |
Returns true if the instruction is a backwards branch.
Definition at line 508 of file goto_program.h.
|
inline |
Definition at line 434 of file goto_program.h.
|
inline |
Definition at line 439 of file goto_program.h.
|
inline |
Definition at line 438 of file goto_program.h.
|
inline |
Definition at line 446 of file goto_program.h.
|
inline |
Definition at line 445 of file goto_program.h.
|
inline |
Definition at line 432 of file goto_program.h.
|
inline |
Definition at line 429 of file goto_program.h.
|
inline |
Definition at line 447 of file goto_program.h.
|
inline |
Definition at line 436 of file goto_program.h.
|
inline |
Definition at line 437 of file goto_program.h.
|
inline |
Definition at line 430 of file goto_program.h.
|
inline |
Definition at line 435 of file goto_program.h.
|
inline |
Definition at line 444 of file goto_program.h.
|
inline |
Is this node a branch target?
Definition at line 402 of file goto_program.h.
|
inline |
Definition at line 433 of file goto_program.h.
|
inline |
Get the return value of a RETURN instruction.
Definition at line 291 of file goto_program.h.
|
inline |
Get the return value of a RETURN instruction.
Definition at line 284 of file goto_program.h.
|
inline |
Set the assignment for ASSIGN.
Definition at line 193 of file goto_program.h.
|
inline |
Set the condition of gotos, assume, assert.
Definition at line 357 of file goto_program.h.
|
inline |
Set the dead statement for DEAD.
Definition at line 269 of file goto_program.h.
|
inline |
Set the declaration for DECL.
Definition at line 235 of file goto_program.h.
|
inline |
Set the function call for FUNCTION_CALL.
Definition at line 313 of file goto_program.h.
|
inline |
Set the statement for OTHER.
Definition at line 327 of file goto_program.h.
|
inline |
Set the return statement for READ.
Definition at line 299 of file goto_program.h.
|
inline |
Sets the first (and only) successor for the usual case of a single target.
Definition at line 383 of file goto_program.h.
|
inline |
Swap two instructions.
Definition at line 481 of file goto_program.h.
|
inline |
Definition at line 520 of file goto_program.h.
Apply given transformer to all expressions; no return value means no change needed.
Definition at line 909 of file goto_program.cpp.
|
inline |
Transforms an existing instruction into a skip, retaining the source_location.
Definition at line 416 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 708 of file goto_program.cpp.
codet goto_programt::instructiont::code |
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 get_condition() to read, and set_condition(c) to write.
Definition at line 341 of file goto_program.h.
std::set<targett> goto_programt::instructiont::incoming_edges |
Definition at line 399 of file goto_program.h.
labelst goto_programt::instructiont::labels |
Definition at line 396 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 498 of file goto_program.h.
unsigned goto_programt::instructiont::loop_number = 0 |
Number unique per function to identify loops.
Definition at line 501 of file goto_program.h.
|
static |
Uniquely identify an invalid target or location.
Definition at line 492 of file goto_program.h.
source_locationt goto_programt::instructiont::source_location |
The location of the instruction in the source file.
Definition at line 334 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 505 of file goto_program.h.
targetst goto_programt::instructiont::targets |
The list of successor instructions.
Definition at line 371 of file goto_program.h.
goto_program_instruction_typet goto_programt::instructiont::type |
What kind of instruction?
Definition at line 337 of file goto_program.h.