cprover
path_lifot Class Reference

LIFO save queue: depth-first search, try to finish paths. More...

#include <path_storage.h>

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

Public Member Functions

void push (const patht &, const patht &) override
 
std::size_t size () const override
 How many paths does this storage contain? More...
 
void clear () override
 Clear all saved paths. More...
 
- Public Member Functions inherited from path_storaget
virtual ~path_storaget ()=default
 
pathtpeek ()
 Reference to the next path to resume. More...
 
virtual void push (const patht &next_instruction, const patht &jump_target)=0
 Add paths to resume to the storage. More...
 
void pop ()
 Remove the next path to resume from the storage. More...
 
bool empty () const
 Is this storage empty? More...
 

Protected Attributes

std::list< path_storaget::patht >::iterator last_peeked
 
std::list< pathtpaths
 

Private Member Functions

pathtprivate_peek () override
 
void private_pop () override
 

Detailed Description

LIFO save queue: depth-first search, try to finish paths.

Definition at line 96 of file path_storage.h.

Member Function Documentation

◆ clear()

void path_lifot::clear ( )
overridevirtual

Clear all saved paths.

This is typically used because we want to terminate symbolic execution early. It doesn't matter too much in terms of memory usage since CBMC typically exits soon after we do that, however it's nice to have tests that check that the worklist is always empty when symex finishes.

Implements path_storaget.

Definition at line 46 of file path_storage.cpp.

References paths.

◆ private_peek()

path_storaget::patht & path_lifot::private_peek ( )
overrideprivatevirtual

Implements path_storaget.

Definition at line 19 of file path_storage.cpp.

References last_peeked, and paths.

◆ private_pop()

void path_lifot::private_pop ( )
overrideprivatevirtual

Implements path_storaget.

Definition at line 34 of file path_storage.cpp.

References last_peeked, paths, and PRECONDITION.

◆ push()

void path_lifot::push ( const patht ,
const patht  
)
override

Definition at line 26 of file path_storage.cpp.

References paths.

◆ size()

std::size_t path_lifot::size ( ) const
overridevirtual

How many paths does this storage contain?

Implements path_storaget.

Definition at line 41 of file path_storage.cpp.

References paths.

Member Data Documentation

◆ last_peeked

std::list<path_storaget::patht>::iterator path_lifot::last_peeked
protected

Definition at line 104 of file path_storage.h.

Referenced by private_peek(), and private_pop().

◆ paths

std::list<patht> path_lifot::paths
protected

Definition at line 105 of file path_storage.h.

Referenced by clear(), private_peek(), private_pop(), push(), and size().


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