cprover
|
#include <scratch_program.h>
Public Member Functions | |
scratch_programt (symbol_tablet &_symbol_table) | |
~scratch_programt () | |
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 () |
![]() | |
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... | |
Public Attributes | |
bool | constant_propagation |
![]() | |
instructionst | instructions |
The list of instructions in the goto program. More... | |
Protected Attributes | |
goto_symex_statet | symex_state |
goto_functionst | functions |
symbol_tablet & | symbol_table |
const namespacet | ns |
symex_target_equationt | equation |
goto_symext | symex |
propt * | satcheck |
bv_pointerst | satchecker |
smt2_dect | z3 |
prop_convt * | checker |
Additional Inherited Members | |
![]() | |
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 |
![]() | |
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... | |
Definition at line 32 of file scratch_program.h.
|
inlineexplicit |
Definition at line 35 of file scratch_program.h.
|
inline |
Definition at line 48 of file scratch_program.h.
References satcheck.
void scratch_programt::append | ( | goto_programt::instructionst & | instructions | ) |
Definition at line 76 of file scratch_program.cpp.
References goto_program_templatet< codet, exprt >::instructions.
Referenced by append_loop(), disjunctive_polynomial_accelerationt::assert_for_values(), polynomial_acceleratort::assert_for_values(), polynomial_acceleratort::check_inductive(), disjunctive_polynomial_accelerationt::find_path(), polynomial_acceleratort::fit_const(), and sat_path_enumeratort::next().
void scratch_programt::append | ( | goto_programt & | program | ) |
Definition at line 175 of file scratch_program.cpp.
References goto_program_templatet< codeT, guardT >::copy_from(), and goto_program_templatet< codet, exprt >::destructive_append().
void scratch_programt::append_loop | ( | goto_programt & | program, |
goto_programt::targett | loop_header | ||
) |
Definition at line 183 of file scratch_program.cpp.
References goto_program_templatet< codet, exprt >::add_instruction(), append(), assume(), goto_program_templatet< codet, exprt >::instructions, SKIP, and goto_program_templatet< codet, exprt >::update().
void scratch_programt::append_path | ( | patht & | path | ) |
Definition at line 151 of file scratch_program.cpp.
References goto_program_templatet< codet, exprt >::add_instruction(), ASSUME, and goto_program_templatet< codet, exprt >::instructions.
Referenced by acceleration_utilst::check_inductive().
goto_programt::targett scratch_programt::assign | ( | const exprt & | lhs, |
const exprt & | rhs | ||
) |
Definition at line 84 of file scratch_program.cpp.
References goto_program_templatet< codet, exprt >::add_instruction(), and ASSIGN.
Referenced by disjunctive_polynomial_accelerationt::accelerate(), polynomial_acceleratort::accelerate(), disjunctive_polynomial_accelerationt::assert_for_values(), polynomial_acceleratort::assert_for_values(), acceleration_utilst::assign_array(), acceleratet::build_state_machine(), acceleration_utilst::do_arrays(), acceleration_utilst::do_assumptions(), acceleration_utilst::do_nonrecursive(), acceleration_utilst::stash_variables(), and polynomial_acceleratort::stash_variables().
goto_programt::targett scratch_programt::assume | ( | const exprt & | guard | ) |
Definition at line 95 of file scratch_program.cpp.
References goto_program_templatet< codet, exprt >::add_instruction(), and ASSUME.
Referenced by append_loop(), acceleration_utilst::assign_array(), acceleratet::build_state_machine(), acceleration_utilst::do_arrays(), acceleration_utilst::do_assumptions(), disjunctive_polynomial_accelerationt::find_path(), disjunctive_polynomial_accelerationt::fit_polynomial(), and sat_path_enumeratort::next().
bool scratch_programt::check_sat | ( | bool | do_slice | ) |
Definition at line 25 of file scratch_program.cpp.
References goto_program_templatet< codet, exprt >::add_instruction(), checker, constant_propagation, goto_symext::constant_propagation, symex_target_equationt::convert(), symex_target_equationt::count_assertions(), decision_proceduret::D_SATISFIABLE, decision_proceduret::dec_solve(), END_FUNCTION, equation, fix_types(), functions, ns, goto_program_templatet< codet, exprt >::output(), remove_skip(), slice(), symex, symex_state, and goto_program_templatet< codet, exprt >::update().
Referenced by acceleration_utilst::check_inductive(), polynomial_acceleratort::check_inductive(), acceleration_utilst::do_assumptions(), disjunctive_polynomial_accelerationt::find_path(), polynomial_acceleratort::fit_const(), disjunctive_polynomial_accelerationt::fit_polynomial(), polynomial_acceleratort::fit_polynomial_sliced(), and sat_path_enumeratort::next().
|
inline |
Definition at line 63 of file scratch_program.h.
Definition at line 67 of file scratch_program.cpp.
References checker, decision_proceduret::get(), ns, goto_symex_statet::rename(), and symex_state.
Referenced by sat_path_enumeratort::build_path(), disjunctive_polynomial_accelerationt::build_path(), acceleration_utilst::extract_polynomial(), polynomial_acceleratort::fit_const(), sat_path_enumeratort::record_path(), and disjunctive_polynomial_accelerationt::record_path().
void scratch_programt::fix_types | ( | ) |
Definition at line 128 of file scratch_program.cpp.
References goto_program_templatet< codet, exprt >::instructions, code_assignt::lhs(), code_assignt::rhs(), to_code_assign(), and exprt::type().
Referenced by disjunctive_polynomial_accelerationt::accelerate(), polynomial_acceleratort::accelerate(), and check_sat().
|
protected |
Definition at line 85 of file scratch_program.h.
Referenced by check_sat(), and eval().
bool scratch_programt::constant_propagation |
Definition at line 72 of file scratch_program.h.
Referenced by check_sat().
|
protected |
Definition at line 79 of file scratch_program.h.
Referenced by check_sat().
|
protected |
Definition at line 76 of file scratch_program.h.
Referenced by check_sat().
|
protected |
Definition at line 78 of file scratch_program.h.
Referenced by check_sat(), and eval().
|
protected |
Definition at line 82 of file scratch_program.h.
Referenced by ~scratch_programt().
|
protected |
Definition at line 83 of file scratch_program.h.
|
protected |
Definition at line 77 of file scratch_program.h.
|
protected |
Definition at line 80 of file scratch_program.h.
Referenced by check_sat().
|
protected |
Definition at line 75 of file scratch_program.h.
Referenced by check_sat(), and eval().
|
protected |
Definition at line 84 of file scratch_program.h.