cprover
|
#include <scratch_program.h>
Public Member Functions | |
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 |
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_programt &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_programt &p) |
Appends the given program, which is destroyed. More... | |
void | destructive_insert (const_targett target, goto_programt &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... | |
std::ostream & | output_instruction (const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &it) 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 () |
const_targett | get_end_function () const |
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... | |
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 |
symbol_tablet | symex_symbol_table |
namespacet | ns |
symex_target_equationt | equation |
path_fifot | path_storage |
optionst | options |
goto_symext | symex |
std::unique_ptr< propt > | satcheck |
bv_pointerst | satchecker |
smt2_dect | z3 |
prop_convt * | checker |
Additional Inherited Members | |
![]() | |
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 std::set< irep_idt > | decl_identifierst |
![]() | |
static const irep_idt | get_function_id (const_targett l) |
static const irep_idt | get_function_id (const goto_programt &p) |
static irep_idt | loop_id (const instructiont &instruction) |
Human-readable loop name. More... | |
Definition at line 36 of file scratch_program.h.
|
inline |
Definition at line 39 of file scratch_program.h.
References options, and optionst::set_option().
void scratch_programt::append | ( | goto_programt::instructionst & | instructions | ) |
Definition at line 75 of file scratch_program.cpp.
References goto_programt::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 174 of file scratch_program.cpp.
References goto_programt::copy_from(), and goto_programt::destructive_append().
void scratch_programt::append_loop | ( | goto_programt & | program, |
goto_programt::targett | loop_header | ||
) |
Definition at line 182 of file scratch_program.cpp.
References goto_programt::add_instruction(), append(), assume(), goto_programt::instructions, SKIP, and goto_programt::update().
void scratch_programt::append_path | ( | patht & | path | ) |
Definition at line 150 of file scratch_program.cpp.
References goto_programt::add_instruction(), ASSUME, and goto_programt::instructions.
Referenced by acceleration_utilst::check_inductive().
goto_programt::targett scratch_programt::assign | ( | const exprt & | lhs, |
const exprt & | rhs | ||
) |
Definition at line 83 of file scratch_program.cpp.
References goto_programt::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 94 of file scratch_program.cpp.
References goto_programt::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_programt::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_programt::output(), remove_skip(), slice(), symex, symex_state, symex_symbol_table, and goto_symext::symex_with_state().
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 68 of file scratch_program.h.
Definition at line 66 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 127 of file scratch_program.cpp.
References goto_programt::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 93 of file scratch_program.h.
Referenced by check_sat(), and eval().
bool scratch_programt::constant_propagation |
Definition at line 77 of file scratch_program.h.
Referenced by check_sat().
|
protected |
Definition at line 85 of file scratch_program.h.
Referenced by check_sat().
|
protected |
Definition at line 81 of file scratch_program.h.
Referenced by check_sat().
|
protected |
Definition at line 84 of file scratch_program.h.
Referenced by check_sat(), and eval().
|
protected |
Definition at line 87 of file scratch_program.h.
Referenced by scratch_programt().
|
protected |
Definition at line 86 of file scratch_program.h.
|
protected |
Definition at line 90 of file scratch_program.h.
|
protected |
Definition at line 91 of file scratch_program.h.
|
protected |
Definition at line 82 of file scratch_program.h.
|
protected |
Definition at line 88 of file scratch_program.h.
Referenced by check_sat().
|
protected |
Definition at line 80 of file scratch_program.h.
Referenced by check_sat(), and eval().
|
protected |
Definition at line 83 of file scratch_program.h.
Referenced by check_sat().
|
protected |
Definition at line 92 of file scratch_program.h.