CBMC
|
#include <unwind.h>
Classes | |
struct | unwind_logt |
Public Types | |
enum class | unwind_strategyt { CONTINUE , PARTIAL , ASSERT_ASSUME , ASSERT_PARTIAL , ASSUME } |
Public Member Functions | |
void | unwind (const irep_idt &function_id, 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 (const irep_idt &function_id, 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 (const irep_idt &function_id, 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 26 of file unwind.cpp.
|
protected |
void goto_unwindt::operator() | ( | goto_functionst & | goto_functions, |
const unwindsett & | unwindset, | ||
const unwind_strategyt | unwind_strategy = unwind_strategyt::PARTIAL |
||
) |
Definition at line 327 of file unwind.cpp.
|
inline |
void goto_unwindt::unwind | ( | const irep_idt & | function_id, |
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 84 of file unwind.cpp.
void goto_unwindt::unwind | ( | const irep_idt & | function_id, |
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 103 of file unwind.cpp.
void goto_unwindt::unwind | ( | const irep_idt & | function_id, |
goto_programt & | goto_program, | ||
const unwindsett & | unwindset, | ||
const unwind_strategyt | unwind_strategy = unwind_strategyt::PARTIAL |
||
) |
Definition at line 282 of file unwind.cpp.
unwind_logt goto_unwindt::unwind_log |