Loading...

Searching...

No Matches

goto_unwindt Class Reference

#include <unwind.h>

+ Collaboration diagram for goto_unwindt:

[フレーム]

[legend]

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 class 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 25 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 326 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 83 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 102 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 281 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:

/home/runner/work/cbmc/cbmc/src/goto-instrument/unwind.h
/home/runner/work/cbmc/cbmc/src/goto-instrument/unwind.cpp

goto_unwindt
Generated by doxygen 1.9.8