CBMC
Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
all_paths_enumeratort Class Reference

#include <all_paths_enumerator.h>

+ Inheritance diagram for all_paths_enumeratort:
+ Collaboration diagram for all_paths_enumeratort:

Public Member Functions

 all_paths_enumeratort (goto_programt &_goto_program, natural_loops_mutablet::natural_loopt &_loop, goto_programt::targett _loop_header)
 
virtual bool next (patht &path)
 
- Public Member Functions inherited from path_enumeratort
virtual ~path_enumeratort ()
 

Protected Member Functions

int backtrack (patht &path)
 
void complete_path (patht &path, int succ)
 
void extend_path (patht &path, goto_programt::targett t, int succ)
 
bool is_looping (patht &path)
 

Protected Attributes

goto_programt & goto_program
 
natural_loops_mutablet::natural_loopt & loop
 
goto_programt::targett loop_header
 
patht last_path
 

Detailed Description

Definition at line 22 of file all_paths_enumerator.h.

Constructor & Destructor Documentation

◆ all_paths_enumeratort()

all_paths_enumeratort::all_paths_enumeratort ( goto_programt &  _goto_program,
natural_loops_mutablet::natural_loopt &  _loop,
goto_programt::targett  _loop_header 
)
inline

Definition at line 25 of file all_paths_enumerator.h.

Member Function Documentation

◆ backtrack()

int all_paths_enumeratort::backtrack ( patht &  path)
protected

Definition at line 59 of file all_paths_enumerator.cpp.

◆ complete_path()

void all_paths_enumeratort::complete_path ( patht &  path,
int  succ 
)
protected

Definition at line 100 of file all_paths_enumerator.cpp.

◆ extend_path()

void all_paths_enumeratort::extend_path ( patht &  path,
goto_programt::targett  t,
int  succ 
)
protected

Definition at line 116 of file all_paths_enumerator.cpp.

◆ is_looping()

bool all_paths_enumeratort::is_looping ( patht &  path)
protected

Definition at line 154 of file all_paths_enumerator.cpp.

◆ next()

bool all_paths_enumeratort::next ( patht &  path)
virtual

Implements path_enumeratort.

Definition at line 14 of file all_paths_enumerator.cpp.

Member Data Documentation

◆ goto_program

goto_programt& all_paths_enumeratort::goto_program
protected

Definition at line 43 of file all_paths_enumerator.h.

◆ last_path

patht all_paths_enumeratort::last_path
protected

Definition at line 47 of file all_paths_enumerator.h.

◆ loop

natural_loops_mutablet::natural_loopt& all_paths_enumeratort::loop
protected

Definition at line 44 of file all_paths_enumerator.h.

◆ loop_header

goto_programt::targett all_paths_enumeratort::loop_header
protected

Definition at line 45 of file all_paths_enumerator.h.

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