cprover
|
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 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. More... | |
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. More... | |
const_targett | const_cast_target (const_targett t) const |
Dummy for templates with possible const contexts. More... | |
template<typename Target > | |
std::list< Target > | get_successors (Target target) const |
Get control-flow successors of a given instruction. More... | |
void | compute_incoming_edges () |
Compute for each instruction the set of instructions it is a successor of. More... | |
void | insert_before_swap (targett target) |
Insertion that preserves jumps to "target". More... | |
void | insert_before_swap (targett target, instructiont &instruction) |
Insertion that preserves jumps to "target". More... | |
void | insert_before_swap (targett target, goto_programt &p) |
Insertion that preserves jumps to "target". More... | |
targett | insert_before (const_targett target) |
Insertion before the instruction pointed-to by the given instruction iterator target . More... | |
targett | insert_before (const_targett target, const instructiont &i) |
Insertion before the instruction pointed-to by the given instruction iterator target . More... | |
targett | insert_after (const_targett target) |
Insertion after the instruction pointed-to by the given instruction iterator target . More... | |
targett | insert_after (const_targett target, const instructiont &i) |
Insertion after the instruction pointed-to by the given instruction iterator target . More... | |
void | destructive_append (goto_programt &p) |
Appends the given program p to *this . p is destroyed. More... | |
void | destructive_insert (const_targett target, goto_programt &p) |
Inserts the given program p before target . More... | |
targett | add (instructiont &&instruction) |
Adds a given instruction at the end. More... | |
targett | add_instruction () |
Adds an instruction at the end. More... | |
targett | add_instruction (goto_program_instruction_typet type) |
Adds an instruction of given type at the end. More... | |
std::ostream & | output (const namespacet &ns, const irep_idt &identifier, std::ostream &out) const |
Output goto program to given stream. More... | |
std::ostream & | output (std::ostream &out) const |
Output goto-program to given stream, using an empty symbol table. More... | |
std::ostream & | output_instruction (const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const |
Output a single instruction. More... | |
void | compute_target_numbers () |
Compute the target numbers. More... | |
void | compute_location_numbers (unsigned &nr) |
Compute location numbers. More... | |
void | compute_location_numbers () |
Compute location numbers. More... | |
void | compute_loop_numbers () |
Compute loop numbers. More... | |
void | update () |
Update all indices. More... | |
bool | empty () const |
Is the program empty? More... | |
goto_programt () | |
Constructor. More... | |
~goto_programt () | |
void | swap (goto_programt &program) |
Swap the goto program. More... | |
void | clear () |
Clear the goto program. More... | |
targett | get_end_function () |
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program. More... | |
const_targett | get_end_function () const |
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program. More... | |
void | copy_from (const goto_programt &src) |
Copy a full goto program, preserving targets. More... | |
bool | has_assertion () const |
Does the goto program have an assertion? More... | |
void | get_decl_identifiers (decl_identifierst &decl_identifiers) const |
get the variables in decl statements More... | |
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. More... | |
void | validate (const namespacet &ns, const validation_modet vm) const |
Check that the goto program is well-formed. More... | |
Public Attributes | |
instructionst | instructions |
The list of instructions in the goto program. More... | |
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 70 of file goto_program.h.
typedef std::list<const_targett> goto_programt::const_targetst |
Definition at line 649 of file goto_program.h.
typedef instructionst::const_iterator goto_programt::const_targett |
Definition at line 647 of file goto_program.h.
typedef std::set<irep_idt> goto_programt::decl_identifierst |
Definition at line 880 of file goto_program.h.
typedef std::list<instructiont> goto_programt::instructionst |
Definition at line 644 of file goto_program.h.
typedef std::list<targett> goto_programt::targetst |
Definition at line 648 of file goto_program.h.
typedef instructionst::iterator goto_programt::targett |
Definition at line 646 of file goto_program.h.
|
delete |
Copying is deleted as this class contains pointers that cannot be copied.
|
inline |
Definition at line 83 of file goto_program.h.
|
inline |
Constructor.
Definition at line 832 of file goto_program.h.
|
inline |
Definition at line 836 of file goto_program.h.
|
inline |
Adds a given instruction at the end.
Definition at line 753 of file goto_program.h.
|
inline |
Adds an instruction at the end.
Definition at line 761 of file goto_program.h.
|
inline |
Adds an instruction of given type at the end.
Definition at line 768 of file goto_program.h.
|
inline |
Clear the goto program.
Definition at line 847 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 712 of file goto_program.cpp.
|
inline |
Compute location numbers.
Definition at line 805 of file goto_program.h.
|
inline |
Compute location numbers.
Definition at line 793 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 568 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 607 of file goto_program.cpp.
|
inline |
Convert a const_targett to a targett - use with care and avoid whenever possible.
Definition at line 656 of file goto_program.h.
|
inline |
Dummy for templates with possible const contexts.
Definition at line 662 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 661 of file goto_program.cpp.
|
inline |
Appends the given program p
to *this
. p
is destroyed.
Definition at line 736 of file goto_program.h.
|
inline |
Inserts the given program p
before target
.
The program p
is destroyed.
Definition at line 744 of file goto_program.h.
|
inline |
Is the program empty?
Definition at line 826 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 1101 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 276 of file goto_program.cpp.
|
inline |
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program.
Definition at line 854 of file goto_program.h.
|
inline |
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program.
Definition at line 865 of file goto_program.h.
std::list< Target > goto_programt::get_successors | ( | Target | target | ) | const |
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 1143 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 702 of file goto_program.cpp.
|
inline |
Insertion after the instruction pointed-to by the given instruction iterator target
.
Definition at line 722 of file goto_program.h.
|
inline |
Insertion after the instruction pointed-to by the given instruction iterator target
.
Definition at line 730 of file goto_program.h.
|
inline |
Insertion before the instruction pointed-to by the given instruction iterator target
.
Definition at line 706 of file goto_program.h.
|
inline |
Insertion before the instruction pointed-to by the given instruction iterator target
.
Definition at line 714 of file goto_program.h.
|
inline |
Insertion that preserves jumps to "target".
Definition at line 673 of file goto_program.h.
|
inline |
Insertion that preserves jumps to "target".
The program p is destroyed.
Definition at line 690 of file goto_program.h.
|
inline |
Insertion that preserves jumps to "target".
The instruction is destroyed.
Definition at line 682 of file goto_program.h.
|
inlinestatic |
Human-readable loop name.
Definition at line 819 of file goto_program.h.
|
inlinestatic |
Definition at line 951 of file goto_program.h.
|
inlinestatic |
Create an assignment instruction.
Definition at line 1082 of file goto_program.h.
|
inlinestatic |
Create an assignment instruction.
Definition at line 1090 of file goto_program.h.
|
inlinestatic |
Definition at line 963 of file goto_program.h.
|
inlinestatic |
Definition at line 993 of file goto_program.h.
|
inlinestatic |
Definition at line 1004 of file goto_program.h.
|
inlinestatic |
Definition at line 941 of file goto_program.h.
|
inlinestatic |
Definition at line 985 of file goto_program.h.
|
inlinestatic |
Definition at line 1099 of file goto_program.h.
|
inlinestatic |
Definition at line 978 of file goto_program.h.
|
inlinestatic |
Definition at line 1015 of file goto_program.h.
|
inlinestatic |
Create a function call instruction.
Definition at line 1107 of file goto_program.h.
|
inlinestatic |
Create a function call instruction.
Definition at line 1115 of file goto_program.h.
|
inlinestatic |
Definition at line 1068 of file goto_program.h.
|
inlinestatic |
Definition at line 1056 of file goto_program.h.
|
inlinestatic |
Definition at line 1049 of file goto_program.h.
|
inlinestatic |
Definition at line 1025 of file goto_program.h.
|
inlinestatic |
Definition at line 1039 of file goto_program.h.
|
inlinestatic |
Definition at line 919 of file goto_program.h.
|
inlinestatic |
Definition at line 971 of file goto_program.h.
|
inlinestatic |
Definition at line 901 of file goto_program.h.
|
inlinestatic |
Definition at line 909 of file goto_program.h.
|
inlinestatic |
Definition at line 930 of file goto_program.h.
|
delete |
|
inline |
Definition at line 88 of file goto_program.h.
std::ostream & goto_programt::output | ( | const namespacet & | ns, |
const irep_idt & | identifier, | ||
std::ostream & | out | ||
) | const |
Output goto program to given stream.
Definition at line 584 of file goto_program.cpp.
std::ostream & goto_programt::output | ( | std::ostream & | out | ) | const |
Output goto-program to given stream, using an empty symbol table.
Definition at line 29 of file goto_program.cpp.
std::ostream & goto_programt::output_instruction | ( | const namespacet & | ns, |
const irep_idt & | identifier, | ||
std::ostream & | out, | ||
const instructionst::value_type & | instruction | ||
) | const |
Output a single instruction.
Writes to out
a two/three line string representation of a given instruction
.
The output is of the format:
ns | the namespace to resolve the expressions in |
identifier | the identifier used to find a symbol to identify the source language |
out | the stream to write the goto string to |
instruction | the instruction to convert |
Definition at line 47 of file goto_program.cpp.
|
inline |
Swap the goto program.
Definition at line 841 of file goto_program.h.
void goto_programt::update | ( | ) |
Update all indices.
Definition at line 576 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 893 of file goto_program.h.
instructionst goto_programt::instructions |
The list of instructions in the goto program.
Definition at line 652 of file goto_program.h.