This class represents an instruction in the GOTO intermediate representation.
More...
|
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.
|
This class represents an instruction in the GOTO intermediate representation.
Three fields are key:
- type: an enum value describing the action performed by this instruction
- guard: an (arbitrarily complex) expression (usually an exprt) of Boolean type
- code: a code statement (usually a goto_instruction_codet)
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:
- GOTO: goto targets if and only if guard is true. More than one target is deprecated. Its semantics was a non-deterministic choice.
- SET_RETURN_VALUE: Set the value returned by return_value(). The control flow is not altered. Many analysis tools remove these instructions before they start.
- DECL: Introduces a symbol denoted by the field 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.
- DEAD: Ends the life of the symbol denoted by the field code. After a DEAD instruction the symbol must be DECL'd again before use.
- FUNCTION_CALL: Invoke the function returned by call_function with the arguments returned by call_arguments, then assign the return value (if any) to call_lhs
- ASSIGN: Update the left-hand side of code (an instance of code_assignt) to the value of the right-hand side.
- OTHER: Execute the code (an instance of goto_instruction_codet of kind ID_fence, ID_printf, ID_array_copy, ID_array_set, ID_input, ID_output, ...).
- ASSUME: This thread of execution waits for guard to evaluate to true. Assume does not "retro-actively" affect the thread or any ASSERTs.
- ASSERT: Using ASSERT instructions is the one and only way to express properties to be verified. An assertion is true / safe if guard is true in all possible executions, otherwise it is false / unsafe. The status of the assertion does not affect execution in any way.
- SKIP, LOCATION: No-op.
- ATOMIC_BEGIN, ATOMIC_END: When a thread executes ATOMIC_BEGIN, no thread other will be able to execute any instruction until the same thread executes ATOMIC_END. Concurrency is not supported by all analysis tools.
- END_FUNCTION: Must occur as the last instruction of the list and nowhere else.
- START_THREAD: Create a new thread and run the code of this function starting from targets[0]. Quite often the instruction pointed by targets[0] will be just a FUNCTION_CALL, followed by an END_THREAD. Concurrency is not supported by all analysis tools.
- END_THREAD: Terminate the calling thread. Concurrency is not supported by all analysis tools.
- THROW: throw exception1, ..., exceptionN where the list of exceptions is extracted from the code field Many analysis tools remove these instructions before they start.
- CATCH, when code.find(ID_exception_list) is non-empty: Establishes that from here to the next occurrence of CATCH with an empty list (see below) if
- 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.
- CATCH, when empty code.find(ID_exception_list) is empty: clears all the catch clauses established as per the above in this function? Many analysis tools remove these instructions before they start.
- INCOMPLETE GOTO: goto for which the target is yet to be determined. The target set shall be empty
Definition at line 179 of file goto_program.h.