cprover
all_paths_enumeratort Class Reference

#include <all_paths_enumerator.h>

Inheritance diagram for all_paths_enumeratort:
[legend]
Collaboration diagram for all_paths_enumeratort:
[legend]

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_programtgoto_program
 
natural_loops_mutablet::natural_looptloop
 
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.

References backtrack(), complete_path(), extend_path(), is_looping(), and next().

Member Function Documentation

§ backtrack()

int all_paths_enumeratort::backtrack ( patht path)
protected

§ complete_path()

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

Definition at line 102 of file all_paths_enumerator.cpp.

References extend_path(), path_nodet::loc, loop, and loop_header.

Referenced by all_paths_enumeratort(), and next().

§ extend_path()

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

§ is_looping()

bool all_paths_enumeratort::is_looping ( patht path)
protected

Definition at line 156 of file all_paths_enumerator.cpp.

References loop_header.

Referenced by all_paths_enumeratort(), and next().

§ next()

bool all_paths_enumeratort::next ( patht path)
virtual

Implements path_enumeratort.

Definition at line 16 of file all_paths_enumerator.cpp.

References backtrack(), complete_path(), is_looping(), last_path, and loop_header.

Referenced by all_paths_enumeratort(), and extend_path().

Member Data Documentation

§ goto_program

goto_programt& all_paths_enumeratort::goto_program
protected

Definition at line 43 of file all_paths_enumerator.h.

Referenced by backtrack(), and extend_path().

§ last_path

patht all_paths_enumeratort::last_path
protected

Definition at line 47 of file all_paths_enumerator.h.

Referenced by next().

§ loop

natural_loops_mutablet::natural_loopt& all_paths_enumeratort::loop
protected

Definition at line 44 of file all_paths_enumerator.h.

Referenced by complete_path().

§ loop_header

goto_programt::targett all_paths_enumeratort::loop_header
protected

Definition at line 45 of file all_paths_enumerator.h.

Referenced by complete_path(), is_looping(), and next().


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