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 unwind_sett &unwind_set, const int k=-1, const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL) |
void | operator() (goto_functionst &goto_functions, const unsigned k, const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL) |
void | operator() (goto_functionst &goto_functions, const unwind_sett &unwind_set, const int k=-1, 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 int global_k, const unwind_sett &unwind_set) 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 59 of file unwind.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), goto_program_templatet< codeT, guardT >::empty(), goto_unwindt::unwind_logt::insert(), goto_program_templatet< codeT, guardT >::instructions, and unwind_log.
Referenced by unwind().
|
protected |
Definition at line 293 of file unwind.cpp.
Referenced by unwind().
|
inline |
void goto_unwindt::operator() | ( | goto_functionst & | goto_functions, |
const unwind_sett & | unwind_set, | ||
const int | k = -1 , |
||
const unwind_strategyt | unwind_strategy = unwind_strategyt::PARTIAL |
||
) |
Definition at line 365 of file unwind.cpp.
References goto_function_templatet< bodyT >::body, goto_function_templatet< bodyT >::body_available(), Forall_goto_functions, and unwind().
|
inline |
Definition at line 76 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 113 of file unwind.cpp.
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 125 of file unwind.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), ASSERT, ASSUME, goto_program_templatet< codeT, guardT >::const_cast_target(), CONTINUE, copy_segment(), goto_program_templatet< codeT, guardT >::destructive_insert(), goto_program_templatet< codeT, guardT >::empty(), Forall_goto_program_instructions, goto_unwindt::unwind_logt::insert(), goto_program_templatet< codeT, guardT >::insert_before(), goto_program_templatet< codeT, guardT >::instructions, exprt::make_false(), PARTIAL, and unwind_log.
void goto_unwindt::unwind | ( | goto_programt & | goto_program, |
const unwind_sett & | unwind_set, | ||
const int | k = -1 , |
||
const unwind_strategyt | unwind_strategy = unwind_strategyt::PARTIAL |
||
) |
Definition at line 316 of file unwind.cpp.
References dstringt::empty(), get_k(), goto_program_templatet< codeT, guardT >::instructions, goto_programt::output_instruction(), and unwind().
unwind_logt goto_unwindt::unwind_log |
Definition at line 110 of file unwind.h.
Referenced by copy_segment(), output_log_json(), and unwind().