CBMC
Classes | Public Types | Public Member Functions | Public Attributes | Protected Member Functions | List of all members
goto_unwindt Class Reference

#include <unwind.h>

+ Collaboration diagram for goto_unwindt:

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)
 

Detailed Description

Definition at line 21 of file unwind.h.

Member Enumeration Documentation

◆ unwind_strategyt

enum goto_unwindt::unwind_strategyt
strong
Enumerator
CONTINUE 
PARTIAL 
ASSERT_ASSUME 
ASSERT_PARTIAL 
ASSUME 

Definition at line 24 of file unwind.h.

Member Function Documentation

◆ copy_segment()

void goto_unwindt::copy_segment ( const goto_programt::const_targett  start,
const goto_programt::const_targett  end,
goto_programt &  goto_program 
)
protected

Definition at line 26 of file unwind.cpp.

◆ get_k()

int goto_unwindt::get_k ( const irep_idt  func,
const unsigned  loop_id,
const unwindsett &  unwindset 
) const
protected

◆ operator()() [1/2]

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.

◆ operator()() [2/2]

void goto_unwindt::operator() ( goto_modelt &  goto_model,
const unwindsett &  unwindset,
const unwind_strategyt  unwind_strategy = unwind_strategyt::PARTIAL 
)
inline

Definition at line 66 of file unwind.h.

◆ output_log_json()

jsont goto_unwindt::output_log_json ( ) const
inline

Definition at line 77 of file unwind.h.

◆ unwind() [1/3]

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.

◆ unwind() [2/3]

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.

◆ unwind() [3/3]

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.

Member Data Documentation

◆ unwind_log

unwind_logt goto_unwindt::unwind_log

Definition at line 115 of file unwind.h.

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