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_after (const_targett target) |
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_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. 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 | update_instructions_function (const irep_idt &function_id) |
Sets the function member of each instruction if not yet set Note that a goto program need not be a goto function and therefore, we cannot do this in update(), but only at the level of of goto_functionst where goto programs are guaranteed to be named functions. 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... | |
Static Public Member Functions | |
static const irep_idt | get_function_id (const_targett l) |
Get the id of the function that contains the instruction pointed-to by the given instruction iterator. More... | |
static const irep_idt | get_function_id (const goto_programt &p) |
Get the id of the function that contains the given goto program. More... | |
static irep_idt | loop_id (const instructiont &instruction) |
Human-readable loop name. 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 72 of file goto_program.h.
typedef std::list<const_targett> goto_programt::const_targetst |
Definition at line 417 of file goto_program.h.
typedef instructionst::const_iterator goto_programt::const_targett |
Definition at line 415 of file goto_program.h.
typedef std::set<irep_idt> goto_programt::decl_identifierst |
Definition at line 680 of file goto_program.h.
typedef std::list<instructiont> goto_programt::instructionst |
Definition at line 412 of file goto_program.h.
typedef std::list<targett> goto_programt::targetst |
Definition at line 416 of file goto_program.h.
typedef instructionst::iterator goto_programt::targett |
Definition at line 414 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 632 of file goto_program.h.
|
inline |
Definition at line 636 of file goto_program.h.
|
inline |
Adds an instruction at the end.
Definition at line 541 of file goto_program.h.
|
inline |
Adds an instruction of given type at the end.
Definition at line 549 of file goto_program.h.
|
inline |
Clear the goto program.
Definition at line 647 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 642 of file goto_program.cpp.
|
inline |
Compute location numbers.
Definition at line 606 of file goto_program.h.
|
inline |
Compute location numbers.
Definition at line 578 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 498 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 537 of file goto_program.cpp.
|
inline |
Convert a const_targett to a targett - use with care and avoid whenever possible.
Definition at line 424 of file goto_program.h.
|
inline |
Dummy for templates with possible const contexts.
Definition at line 430 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 591 of file goto_program.cpp.
|
inline |
Appends the given program p
to *this
. p
is destroyed.
Definition at line 524 of file goto_program.h.
|
inline |
Inserts the given program p
before target
.
The program p
is destroyed.
Definition at line 532 of file goto_program.h.
|
inline |
Is the program empty?
Definition at line 626 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 832 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 222 of file goto_program.cpp.
|
inline |
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program.
Definition at line 654 of file goto_program.h.
|
inline |
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program.
Definition at line 665 of file goto_program.h.
|
inlinestatic |
Get the id of the function that contains the given goto program.
p | the goto program |
Definition at line 463 of file goto_program.h.
|
inlinestatic |
Get the id of the function that contains the instruction pointed-to by the given instruction iterator.
l | instruction iterator |
Definition at line 440 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 715 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 632 of file goto_program.cpp.
|
inline |
Insertion after the instruction pointed-to by the given instruction iterator target
.
Definition at line 518 of file goto_program.h.
|
inline |
Insertion before the instruction pointed-to by the given instruction iterator target
.
Definition at line 510 of file goto_program.h.
|
inline |
Insertion that preserves jumps to "target".
Definition at line 477 of file goto_program.h.
|
inline |
Insertion that preserves jumps to "target".
The program p is destroyed.
Definition at line 494 of file goto_program.h.
|
inline |
Insertion that preserves jumps to "target".
The instruction is destroyed.
Definition at line 486 of file goto_program.h.
|
inlinestatic |
Human-readable loop name.
Definition at line 619 of file goto_program.h.
|
delete |
|
inline |
Definition at line 90 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 514 of file goto_program.cpp.
|
inline |
Output goto-program to given stream.
Definition at line 562 of file goto_program.h.
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 37 of file goto_program.cpp.
|
inline |
Swap the goto program.
Definition at line 641 of file goto_program.h.
void goto_programt::update | ( | ) |
Update all indices.
Definition at line 506 of file goto_program.cpp.
|
inline |
Sets the function
member of each instruction if not yet set Note that a goto program need not be a goto function and therefore, we cannot do this in update(), but only at the level of of goto_functionst where goto programs are guaranteed to be named functions.
Definition at line 594 of file goto_program.h.
|
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 693 of file goto_program.h.
instructionst goto_programt::instructions |
The list of instructions in the goto program.
Definition at line 420 of file goto_program.h.