cprover
path_fifot Class Reference

FIFO save queue: paths are resumed in the order that they were saved. More...

#include <path_storage.h>

+ Inheritance diagram for path_fifot:
+ Collaboration diagram for path_fifot:

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< pathtpaths
 

Private Member Functions

pathtprivate_peek () override
 
void private_pop () override
 

Detailed Description

FIFO save queue: paths are resumed in the order that they were saved.

Definition at line 113 of file path_storage.h.

Member Function Documentation

◆ clear()

void path_fifot::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 77 of file path_storage.cpp.

◆ private_peek()

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

Implements path_storaget.

Definition at line 54 of file path_storage.cpp.

◆ private_pop()

void path_fifot::private_pop ( )
overrideprivatevirtual

Implements path_storaget.

Definition at line 67 of file path_storage.cpp.

◆ push()

void path_fifot::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 59 of file path_storage.cpp.

◆ size()

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

How many paths does this storage contain?

Implements path_storaget.

Definition at line 72 of file path_storage.cpp.

Member Data Documentation

◆ paths

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

Definition at line 121 of file path_storage.h.


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