|
| | scratch_programt (symbol_table_baset &_symbol_table, message_handlert &mh, guard_managert &guard_manager) |
| |
| 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, guard_managert &guard_manager) |
| |
| bool | check_sat (guard_managert &guard_manager) |
| |
| 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_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 (std::ostream &out) const |
| | Output goto-program to given stream. 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...
|
| |
|
| 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 |
| |
| static irep_idt | loop_id (const irep_idt &function_id, const instructiont &instruction) |
| | Human-readable loop name. More...
|
| |
| 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. More...
|
| |
| static instructiont | make_assignment (exprt lhs, exprt rhs, const source_locationt &l=source_locationt::nil()) |
| | Create an assignment instruction. More...
|
| |
| 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. More...
|
| |
| 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. More...
|
| |
Definition at line 60 of file scratch_program.h.
Inheritance diagram for scratch_programt: