cprover
|
#include <unwind.h>
Classes | |
struct | unwind_logt |
Public Types | |
enum | unwind_strategyt { unwind_strategyt::CONTINUE, unwind_strategyt::PARTIAL, unwind_strategyt::ASSERT, unwind_strategyt::ASSUME } |
Public Member Functions | |
void | unwind (goto_programt &goto_program, const goto_programt::const_targett loop_head, const goto_programt::const_targett loop_exit, const unsigned k, const unwind_strategyt unwind_strategy) |
void | unwind (goto_programt &goto_program, const goto_programt::const_targett loop_head, const goto_programt::const_targett loop_exit, const unsigned k, const unwind_strategyt unwind_strategy, std::vector< goto_programt::targett > &iteration_points) |
void | unwind (goto_programt &goto_program, const unwindsett &unwindset, const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL) |
void | operator() (goto_functionst &, const unwindsett &unwindset, const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL) |
void | operator() (goto_modelt &goto_model, const unwindsett &unwindset, const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL) |
jsont | output_log_json () const |
Public Attributes | |
unwind_logt | unwind_log |
Protected Member Functions | |
int | get_k (const irep_idt func, const unsigned loop_id, const unwindsett &unwindset) const |
void | copy_segment (const goto_programt::const_targett start, const goto_programt::const_targett end, goto_programt &goto_program) |
|
strong |
|
protected |
Definition at line 25 of file unwind.cpp.
References goto_programt::add_instruction(), goto_programt::empty(), goto_program, goto_unwindt::unwind_logt::insert(), goto_programt::instructions, and unwind_log.
Referenced by unwind().
|
protected |
void goto_unwindt::operator() | ( | goto_functionst & | goto_functions, |
const unwindsett & | unwindset, | ||
const unwind_strategyt | unwind_strategy = unwind_strategyt::PARTIAL |
||
) |
Definition at line 307 of file unwind.cpp.
References Forall_goto_functions, goto_program, and unwind().
Referenced by operator()().
|
inline |
Definition at line 59 of file unwind.h.
References goto_modelt::goto_functions, and operator()().
|
inline |
Definition at line 70 of file unwind.h.
References goto_unwindt::unwind_logt::output_log_json(), and unwind_log.
Referenced by goto_instrument_parse_optionst::doit().
void goto_unwindt::unwind | ( | goto_programt & | goto_program, |
const goto_programt::const_targett | loop_head, | ||
const goto_programt::const_targett | loop_exit, | ||
const unsigned | k, | ||
const unwind_strategyt | unwind_strategy | ||
) |
Definition at line 79 of file unwind.cpp.
References goto_program.
Referenced by operator()(), k_inductiont::process_loop(), and unwind().
void goto_unwindt::unwind | ( | goto_programt & | goto_program, |
const goto_programt::const_targett | loop_head, | ||
const goto_programt::const_targett | loop_exit, | ||
const unsigned | k, | ||
const unwind_strategyt | unwind_strategy, | ||
std::vector< goto_programt::targett > & | iteration_points | ||
) |
Definition at line 91 of file unwind.cpp.
References goto_programt::add_instruction(), ASSERT, ASSUME, goto_programt::const_cast_target(), CONTINUE, copy_segment(), goto_programt::destructive_insert(), goto_programt::empty(), Forall_goto_program_instructions, goto_program, goto_unwindt::unwind_logt::insert(), goto_programt::insert_before(), goto_programt::instructions, exprt::make_false(), PARTIAL, UNREACHABLE, and unwind_log.
void goto_unwindt::unwind | ( | goto_programt & | goto_program, |
const unwindsett & | unwindset, | ||
const unwind_strategyt | unwind_strategy = unwind_strategyt::PARTIAL |
||
) |
Definition at line 259 of file unwind.cpp.
References dstringt::empty(), unwindsett::get_limit(), goto_program, id2string(), goto_programt::instructions, goto_programt::output_instruction(), to_string(), and unwind().
unwind_logt goto_unwindt::unwind_log |
Definition at line 104 of file unwind.h.
Referenced by copy_segment(), output_log_json(), and unwind().