cprover
|
A specialization of goto_program_templatet over goto programs in which instructions have codet type. More...
#include <goto_program.h>
Public Types | |
typedef std::set< irep_idt > | decl_identifierst |
![]() | |
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 |
Public Member Functions | |
std::ostream & | output_instruction (const class namespacet &ns, const irep_idt &identifier, std::ostream &out, instructionst::const_iterator it) const |
See below. More... | |
std::ostream & | output_instruction (const class namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructiont &instruction) const |
goto_programt () | |
goto_programt (const goto_programt &)=delete | |
goto_programt & | operator= (const goto_programt &)=delete |
goto_programt (goto_programt &&other) | |
goto_programt & | operator= (goto_programt &&other) |
void | get_decl_identifiers (decl_identifierst &decl_identifiers) const |
![]() | |
goto_program_templatet (const goto_program_templatet &)=delete | |
Copying is deleted as this class contains pointers that cannot be copied. More... | |
goto_program_templatet (goto_program_templatet &&other) | |
goto_program_templatet () | |
Constructor. More... | |
goto_program_templatet & | operator= (const goto_program_templatet &)=delete |
goto_program_templatet & | operator= (goto_program_templatet &&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... | |
std::list< Target > | get_successors (Target target) const |
void | compute_incoming_edges () |
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_program_templatet< codet, exprt > &p) |
Insertion that preserves jumps to "target". More... | |
targett | insert_before (const_targett target) |
Insertion before the given target. More... | |
targett | insert_after (const_targett target) |
Insertion after the given target. More... | |
void | destructive_append (goto_program_templatet< codet, exprt > &p) |
Appends the given program, which is destroyed. More... | |
void | destructive_insert (const_targett target, goto_program_templatet< codet, exprt > &p) |
Inserts the given program at the given location. 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... | |
virtual std::ostream & | output_instruction (const namespacet &ns, const irep_idt &identifier, std::ostream &out, typename instructionst::const_iterator it) const=0 |
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... | |
virtual | ~goto_program_templatet () |
void | swap (goto_program_templatet< codet, exprt > &program) |
Swap the goto program. More... | |
void | clear () |
Clear the goto program. More... | |
targett | get_end_function () |
void | copy_from (const goto_program_templatet< codet, exprt > &src) |
Copy a full goto program, preserving targets. More... | |
bool | has_assertion () const |
Does the goto program have an assertion? More... | |
Additional Inherited Members | |
![]() | |
static const irep_idt | get_function_id (const_targett l) |
static const irep_idt | get_function_id (const goto_program_templatet< codet, exprt > &p) |
static irep_idt | loop_id (const_targett target) |
Human-readable loop name. More... | |
![]() | |
instructionst | instructions |
The list of instructions in the goto program. More... | |
A specialization of goto_program_templatet over goto programs in which instructions have codet type.
Definition at line 24 of file goto_program.h.
typedef std::set<irep_idt> goto_programt::decl_identifierst |
Definition at line 64 of file goto_program.h.
|
inline |
Definition at line 39 of file goto_program.h.
References operator=().
|
delete |
|
inline |
Definition at line 52 of file goto_program.h.
void goto_programt::get_decl_identifiers | ( | decl_identifierst & | decl_identifiers | ) | const |
Definition at line 218 of file goto_program.cpp.
References forall_goto_program_instructions, and to_symbol_expr().
Referenced by invariant_propagationt::add_objects(), value_set_analysis_fit::add_vars(), value_set_analysis_fivrt::add_vars(), value_set_analysis_fivrnst::add_vars(), and get_local_identifiers().
|
delete |
Referenced by goto_programt().
|
inline |
Definition at line 57 of file goto_program.h.
References goto_program_templatet< codeT, guardT >::operator=().
std::ostream & goto_programt::output_instruction | ( | const class namespacet & | ns, |
const irep_idt & | identifier, | ||
std::ostream & | out, | ||
instructionst::const_iterator | it | ||
) | const |
See below.
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 |
it | an iterator pointing to the instruction to convert |
Definition at line 27 of file goto_program.cpp.
References source_locationt::as_string(), ASSERT, ASSIGN, ASSUME, ATOMIC_BEGIN, ATOMIC_END, CATCH, goto_program_templatet< codeT, guardT >::instructiont::code, comment(), DEAD, DECL, END_FUNCTION, END_THREAD, from_expr(), FUNCTION_CALL, source_locationt::get_comment(), GOTO, goto_program_templatet< codeT, guardT >::instructiont::guard, goto_program_templatet< codeT, guardT >::instructiont::is_assume(), irept::is_nil(), goto_program_templatet< codeT, guardT >::instructiont::is_target(), goto_program_templatet< codeT, guardT >::instructiont::labels, LOCATION, goto_program_templatet< codeT, guardT >::instructiont::location_number, NO_INSTRUCTION_TYPE, OTHER, RETURN, SKIP, goto_program_templatet< codeT, guardT >::instructiont::source_location, START_THREAD, goto_program_templatet< codeT, guardT >::instructiont::target_number, goto_program_templatet< codeT, guardT >::instructiont::targets, THROW, and goto_program_templatet< codeT, guardT >::instructiont::type.
Referenced by enumerating_loop_accelerationt::accelerate(), disjunctive_polynomial_accelerationt::accelerate(), polynomial_acceleratort::accelerate(), add_to_json(), goto_instrument_parse_optionst::doit(), goto_inlinet::expand_function_call(), value_set_analysis_fivrt::output(), value_set_analysis_fivrnst::output(), static_analysis_baset::output(), ai_baset::output(), output_dead_plain(), unified_difft::output_diff(), change_impactt::output_instruction(), ai_baset::output_json(), output_path(), ai_baset::output_xml(), and goto_unwindt::unwind().
std::ostream& goto_programt::output_instruction | ( | const class namespacet & | ns, |
const irep_idt & | identifier, | ||
std::ostream & | out, | ||
const instructiont & | instruction | ||
) | const |