cprover
goto_unwindt Class Reference

#include <unwind.h>

Collaboration diagram for goto_unwindt:
[legend]

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)
 

Detailed Description

Definition at line 27 of file unwind.h.

Member Enumeration Documentation

§ unwind_strategyt

Enumerator
CONTINUE 
PARTIAL 
ASSERT 
ASSUME 

Definition at line 30 of file unwind.h.

Member Function Documentation

§ copy_segment()

§ get_k()

int goto_unwindt::get_k ( const irep_idt  func,
const unsigned  loop_id,
const int  global_k,
const unwind_sett unwind_set 
) const
protected

Definition at line 293 of file unwind.cpp.

Referenced by unwind().

§ operator()() [1/2]

void goto_unwindt::operator() ( goto_functionst goto_functions,
const unsigned  k,
const unwind_strategyt  unwind_strategy = unwind_strategyt::PARTIAL 
)
inline

Definition at line 59 of file unwind.h.

References PARTIAL.

§ operator()() [2/2]

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 
)

§ output_log_json()

jsont goto_unwindt::output_log_json ( ) const
inline

§ unwind() [1/3]

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().

§ unwind() [2/3]

§ unwind() [3/3]

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 
)

Member Data Documentation

§ unwind_log

unwind_logt goto_unwindt::unwind_log

Definition at line 110 of file unwind.h.

Referenced by copy_segment(), output_log_json(), and unwind().


The documentation for this class was generated from the following files: