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:
+ Collaboration diagram for path_lifot:

Public Member Functions

void push (const patht &, const patht &) override
 Add paths to resume to the storage. More...
 
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...
 
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.

◆ private_peek()

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

Implements path_storaget.

Definition at line 19 of file path_storage.cpp.

◆ private_pop()

void path_lifot::private_pop ( )
overrideprivatevirtual

Implements path_storaget.

Definition at line 34 of file path_storage.cpp.

◆ push()

void path_lifot::push ( const patht next_instruction,
const patht jump_target 
)
overridevirtual

Add paths to resume to the storage.

Symbolic execution is suspended when we reach a conditional goto instruction with two successors. Thus, we always add a pair of paths to the path storage.

Parameters
next_instructionthe instruction following the goto instruction
jump_targetthe target instruction of the goto instruction

Implements path_storaget.

Definition at line 26 of file path_storage.cpp.

◆ 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.

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.

◆ paths

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

Definition at line 105 of file path_storage.h.


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