|
| scratch_programt (symbol_tablet &_symbol_table, message_handlert &mh) |
|
void | append (goto_programt::instructionst &instructions) |
|
void | append (goto_programt &program) |
|
void | append_path (patht &path) |
|
void | append_loop (goto_programt &program, goto_programt::targett loop_header) |
|
targett | assign (const exprt &lhs, const exprt &rhs) |
|
targett | assume (const exprt &guard) |
|
bool | check_sat (bool do_slice) |
|
bool | check_sat () |
|
exprt | eval (const exprt &e) |
|
void | fix_types () |
|
| 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...
|
|
Definition at line 36 of file scratch_program.h.