CBMC
|
A generic container class for the GOTO intermediate representation of one function. More...
#include <goto_program.h>
Classes | |
class | instructiont |
This class represents an instruction in the GOTO intermediate representation. More... | |
Public Types | |
typedef std::list< instructiont > | instructionst |
typedef instructionst::iterator | targett |
typedef instructionst::const_iterator | const_targett |
typedef std::list< targett > | targetst |
typedef std::list< const_targett > | const_targetst |
typedef instructiont::target_less_than | target_less_than |
typedef std::set< irep_idt > | decl_identifierst |
Public Member Functions | |
goto_programt (const goto_programt &)=delete | |
Copying is deleted as this class contains pointers that cannot be copied. | |
goto_programt & | operator= (const goto_programt &)=delete |
goto_programt (goto_programt &&other) | |
goto_programt & | operator= (goto_programt &&other) |
targett | const_cast_target (const_targett t) |
Convert a const_targett to a targett - use with care and avoid whenever possible. | |
const_targett | const_cast_target (const_targett t) const |
Dummy for templates with possible const contexts. | |
template<typename Target > | |
std::list< Target > | get_successors (Target target) const |
Get control-flow successors of a given instruction. | |
void | compute_incoming_edges () |
Compute for each instruction the set of instructions it is a successor of. | |
void | insert_before_swap (targett target) |
Insertion that preserves jumps to "target". | |
void | insert_before_swap (targett target, instructiont &instruction) |
Insertion that preserves jumps to "target". | |
void | insert_before_swap (targett target, goto_programt &p) |
Insertion that preserves jumps to "target". | |
targett | insert_before (const_targett target) |
Insertion before the instruction pointed-to by the given instruction iterator target . | |
targett | insert_before (const_targett target, const instructiont &i) |
Insertion before the instruction pointed-to by the given instruction iterator target . | |
targett | insert_after (const_targett target) |
Insertion after the instruction pointed-to by the given instruction iterator target . | |
targett | insert_after (const_targett target, const instructiont &i) |
Insertion after the instruction pointed-to by the given instruction iterator target . | |
void | destructive_append (goto_programt &p) |
Appends the given program p to *this . p is destroyed. | |
void | destructive_insert (const_targett target, goto_programt &p) |
Inserts the given program p before target . | |
targett | add (instructiont &&instruction) |
Adds a given instruction at the end. | |
targett | add_instruction () |
Adds an instruction at the end. | |
targett | add_instruction (goto_program_instruction_typet type) |
Adds an instruction of given type at the end. | |
std::ostream & | output (std::ostream &out) const |
Output goto-program to given stream. | |
void | compute_target_numbers () |
Compute the target numbers. | |
void | compute_location_numbers (unsigned &nr) |
Compute location numbers. | |
void | compute_location_numbers () |
Compute location numbers. | |
void | compute_loop_numbers () |
Compute loop numbers. | |
void | update () |
Update all indices. | |
bool | empty () const |
Is the program empty? | |
goto_programt () | |
Constructor. | |
~goto_programt () | |
void | swap (goto_programt &program) |
Swap the goto program. | |
void | clear () |
Clear the goto program. | |
targett | get_end_function () |
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program. | |
const_targett | get_end_function () const |
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program. | |
void | copy_from (const goto_programt &src) |
Copy a full goto program, preserving targets. | |
bool | has_assertion () const |
Does the goto program have an assertion? | |
void | get_decl_identifiers (decl_identifierst &decl_identifiers) const |
get the variables in decl statements | |
bool | equals (const goto_programt &other) const |
Syntactic equality: two goto_programt are equal if, and only if, they have the same number of instructions, each pair of instructions compares equal, and relative jumps have the same distance. | |
void | validate (const namespacet &ns, const validation_modet vm) const |
Check that the goto program is well-formed. | |
Public Attributes | |
instructionst | instructions |
The list of instructions in the goto program. | |
A generic container class for the GOTO intermediate representation of one function.
A function is represented by a std::list of instructions. Execution starts in the first instruction of the list. Then, the execution of the i-th instruction is followed by the execution of the (i+1)-th instruction unless instruction i jumps to some other instruction in the list. See the internal class instructiont for additional details
Although it is straightforward to compute the control flow graph (CFG) of a function from the list of instructions and the goto target locations in instructions, the GOTO intermediate representation is not regarded as the CFG of a function. See instead the class cfg_baset, which is based on grapht and allows for easier implementation of generic graph algorithms (e.g., dominator analysis).
Definition at line 72 of file goto_program.h.
typedef std::list<const_targett> goto_programt::const_targetst |
Definition at line 617 of file goto_program.h.
typedef instructionst::const_iterator goto_programt::const_targett |
Definition at line 615 of file goto_program.h.
typedef std::set<irep_idt> goto_programt::decl_identifierst |
Definition at line 853 of file goto_program.h.
typedef std::list<instructiont> goto_programt::instructionst |
Definition at line 612 of file goto_program.h.
Definition at line 619 of file goto_program.h.
typedef std::list<targett> goto_programt::targetst |
Definition at line 616 of file goto_program.h.
typedef instructionst::iterator goto_programt::targett |
Definition at line 614 of file goto_program.h.
|
delete |
Copying is deleted as this class contains pointers that cannot be copied.
|
inline |
Definition at line 85 of file goto_program.h.
|
inline |
Constructor.
Definition at line 805 of file goto_program.h.
|
inline |
Definition at line 809 of file goto_program.h.
|
inline |
Adds a given instruction at the end.
Definition at line 739 of file goto_program.h.
|
inline |
Adds an instruction at the end.
Definition at line 747 of file goto_program.h.
|
inline |
Adds an instruction of given type at the end.
Definition at line 754 of file goto_program.h.
|
inline |
Clear the goto program.
Definition at line 820 of file goto_program.h.
void goto_programt::compute_incoming_edges | ( | ) |
Compute for each instruction the set of instructions it is a successor of.
Definition at line 752 of file goto_program.cpp.
|
inline |
Compute location numbers.
Definition at line 778 of file goto_program.h.
Compute location numbers.
Definition at line 766 of file goto_program.h.
void goto_programt::compute_loop_numbers | ( | ) |
Compute loop numbers.
Assign each loop in the goto program a unique index.
Every backwards goto is considered a loop. The loops are numbered starting from zero and in the order they appear in the goto program.
Definition at line 611 of file goto_program.cpp.
void goto_programt::compute_target_numbers | ( | ) |
Compute the target numbers.
Assign each target (i.e., an instruction that is in the targets
list of another instruction) a unique index.
Instructions that are not targets get target number instructiont::nil_target. The targets are numbered starting from one and in the order they appear in the goto program. An instruction is considered a target if it is the target of a control-flow instruction (either GOTO or START_THREAD), i.e., it is contained in the targets
list of those instructions. Instructions that are reached via straight-line control flow (fall-through for GOTO instructions) only are not considered targets.
Definition at line 647 of file goto_program.cpp.
|
inline |
Convert a const_targett to a targett - use with care and avoid whenever possible.
Definition at line 626 of file goto_program.h.
|
inline |
Dummy for templates with possible const contexts.
Definition at line 632 of file goto_program.h.
void goto_programt::copy_from | ( | const goto_programt & | src | ) |
Copy a full goto program, preserving targets.
Copy other goto program into this goto program.
The current goto program is cleared, and targets are adjusted as needed
src | the goto program to copy from |
Definition at line 701 of file goto_program.cpp.
|
inline |
Appends the given program p
to *this
. p
is destroyed.
Definition at line 722 of file goto_program.h.
|
inline |
Inserts the given program p
before target
.
The program p
is destroyed.
Definition at line 730 of file goto_program.h.
|
inline |
Is the program empty?
Definition at line 799 of file goto_program.h.
bool goto_programt::equals | ( | const goto_programt & | other | ) | const |
Syntactic equality: two goto_programt are equal if, and only if, they have the same number of instructions, each pair of instructions compares equal, and relative jumps have the same distance.
Definition at line 1140 of file goto_program.cpp.
void goto_programt::get_decl_identifiers | ( | decl_identifierst & | decl_identifiers | ) | const |
get the variables in decl statements
Definition at line 319 of file goto_program.cpp.
|
inline |
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program.
Definition at line 827 of file goto_program.h.
|
inline |
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program.
Definition at line 838 of file goto_program.h.
Get control-flow successors of a given instruction.
The instruction is represented by a pointer target
of type Target
. An instruction has either 0, 1, or 2 successors (more than two successors is deprecated). For example, an ASSUME
instruction with the guard
being a false_exprt
has 0 successors, and ASSIGN
instruction has 1 successor, and a GOTO
instruction with the guard
not being a true_exprt
has 2 successors.
Target | type used to represent a pointer to an instruction in a goto program |
target | pointer to the instruction of which to get the successors of |
Definition at line 1126 of file goto_program.h.
bool goto_programt::has_assertion | ( | ) | const |
Does the goto program have an assertion?
Returns true if the goto program includes an ASSERT
instruction the guard of which is not trivially true.
Definition at line 742 of file goto_program.cpp.
|
inline |
Insertion after the instruction pointed-to by the given instruction iterator target
.
Definition at line 708 of file goto_program.h.
|
inline |
Insertion after the instruction pointed-to by the given instruction iterator target
.
Definition at line 716 of file goto_program.h.
|
inline |
Insertion before the instruction pointed-to by the given instruction iterator target
.
Definition at line 692 of file goto_program.h.
|
inline |
Insertion before the instruction pointed-to by the given instruction iterator target
.
Definition at line 700 of file goto_program.h.
Insertion that preserves jumps to "target".
Definition at line 643 of file goto_program.h.
|
inline |
Insertion that preserves jumps to "target".
The program p is destroyed.
Definition at line 676 of file goto_program.h.
|
inline |
Insertion that preserves jumps to "target".
The instruction is destroyed.
Turns:
Into:
So that jumps to a
now jump to the newly inserted i
.
Definition at line 668 of file goto_program.h.
|
inlinestatic |
Human-readable loop name.
Definition at line 792 of file goto_program.h.
|
inlinestatic |
Definition at line 933 of file goto_program.h.
|
inlinestatic |
Create an assignment instruction.
Definition at line 1065 of file goto_program.h.
|
inlinestatic |
Create an assignment instruction.
Definition at line 1073 of file goto_program.h.
|
inlinestatic |
Definition at line 945 of file goto_program.h.
|
inlinestatic |
Definition at line 979 of file goto_program.h.
|
inlinestatic |
Definition at line 990 of file goto_program.h.
|
inlinestatic |
Definition at line 923 of file goto_program.h.
|
inlinestatic |
Definition at line 971 of file goto_program.h.
|
inlinestatic |
Definition at line 1082 of file goto_program.h.
|
inlinestatic |
Definition at line 964 of file goto_program.h.
|
inlinestatic |
Definition at line 1001 of file goto_program.h.
|
inlinestatic |
Create a function call instruction.
Definition at line 1090 of file goto_program.h.
|
inlinestatic |
Create a function call instruction.
Definition at line 1098 of file goto_program.h.
|
inlinestatic |
Definition at line 1051 of file goto_program.h.
|
inlinestatic |
Definition at line 1039 of file goto_program.h.
|
static |
Definition at line 33 of file goto_program.cpp.
|
inlinestatic |
Definition at line 1011 of file goto_program.h.
|
inlinestatic |
Definition at line 1025 of file goto_program.h.
|
inlinestatic |
Definition at line 901 of file goto_program.h.
|
inlinestatic |
Definition at line 957 of file goto_program.h.
|
staticdelete |
|
inlinestatic |
Definition at line 874 of file goto_program.h.
|
inlinestatic |
Definition at line 891 of file goto_program.h.
|
inlinestatic |
Definition at line 912 of file goto_program.h.
|
delete |
|
inline |
Definition at line 90 of file goto_program.h.
std::ostream & goto_programt::output | ( | std::ostream & | out | ) | const |
Output goto-program to given stream.
Definition at line 627 of file goto_program.cpp.
|
inline |
Swap the goto program.
Definition at line 814 of file goto_program.h.
void goto_programt::update | ( | ) |
Update all indices.
Definition at line 619 of file goto_program.cpp.
|
inline |
Check that the goto program is well-formed.
The validation mode indicates whether well-formedness check failures are reported via DATA_INVARIANT violations or exceptions.
Definition at line 866 of file goto_program.h.
instructionst goto_programt::instructions |
The list of instructions in the goto program.
Definition at line 622 of file goto_program.h.