goto_unwindt Class Reference

#include <unwind.h>

Collaboration diagram for goto_unwindt:

Classes
struct	unwind_logt

Public Types
enum	unwind_strategyt {   unwind_strategyt::CONTINUE, unwind_strategyt::PARTIAL, unwind_strategyt::ASSERT_ASSUME, unwind_strategyt::ASSERT_PARTIAL,   unwind_strategyt::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 320 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 82 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 101 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 275 of file unwind.cpp.

Member Data Documentation

unwind_log

unwind_logt goto_unwindt::unwind_log

Definition at line 111 of file unwind.h.

---

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

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