A generic container class for the GOTO intermediate representation of one function.
More...
|
| 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.
|
|
static irep_idt | loop_id (const irep_idt &function_id, const instructiont &instruction) |
| Human-readable loop name.
|
static instructiont | make_set_return_value (exprt return_value, const source_locationt &l=source_locationt::nil()) |
static instructiont | make_set_return_value (const code_returnt &code, const source_locationt &l=source_locationt::nil())=delete |
static instructiont | make_skip (const source_locationt &l=source_locationt::nil()) |
static instructiont | make_location (const source_locationt &l) |
static instructiont | make_throw (const source_locationt &l=source_locationt::nil()) |
static instructiont | make_catch (const source_locationt &l=source_locationt::nil()) |
static instructiont | make_assertion (const exprt &g, const source_locationt &l=source_locationt::nil()) |
static instructiont | make_assumption (const exprt &g, const source_locationt &l=source_locationt::nil()) |
static instructiont | make_other (const goto_instruction_codet &_code, const source_locationt &l=source_locationt::nil()) |
static instructiont | make_decl (const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil()) |
static instructiont | make_dead (const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil()) |
static instructiont | make_atomic_begin (const source_locationt &l=source_locationt::nil()) |
static instructiont | make_atomic_end (const source_locationt &l=source_locationt::nil()) |
static instructiont | make_end_function (const source_locationt &l=source_locationt::nil()) |
static instructiont | make_incomplete_goto (const exprt &_cond, const source_locationt &l=source_locationt::nil()) |
static instructiont | make_incomplete_goto (const source_locationt &l=source_locationt::nil()) |
static instructiont | make_incomplete_goto (const code_gotot &, const source_locationt &=source_locationt::nil()) |
static instructiont | make_goto (targett _target, const source_locationt &l=source_locationt::nil()) |
static instructiont | make_goto (targett _target, const exprt &g, const source_locationt &l=source_locationt::nil()) |
static instructiont | make_assignment (const code_assignt &_code, const source_locationt &l=source_locationt::nil()) |
| Create an assignment instruction.
|
static instructiont | make_assignment (exprt lhs, exprt rhs, const source_locationt &l=source_locationt::nil()) |
| Create an assignment instruction.
|
static instructiont | make_decl (const code_declt &_code, const source_locationt &l=source_locationt::nil()) |
static instructiont | make_function_call (const code_function_callt &_code, const source_locationt &l=source_locationt::nil()) |
| Create a function call instruction.
|
static instructiont | make_function_call (exprt lhs, exprt function, code_function_callt::argumentst arguments, const source_locationt &l=source_locationt::nil()) |
| Create a function call instruction.
|
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 71 of file goto_program.h.
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.
template<typename Target>
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.
- Template Parameters
-
Target | type used to represent a pointer to an instruction in a goto program |
- Parameters
-
target | pointer to the instruction of which to get the successors of |
- Returns
- List of control-flow successors of the pointed-to goto program instruction
Definition at line 1125 of file goto_program.h.