cprover
path_storaget Class Referenceabstract

Storage for symbolic execution paths to be resumed later. More...

#include <path_storage.h>

Inheritance diagram for path_storaget:
[legend]

Classes

struct  patht
 Information saved at a conditional goto to resume execution. More...
 

Public Member Functions

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...
 
virtual std::size_t size () const =0
 How many paths does this storage contain? More...
 
bool empty () const
 Is this storage empty? More...
 

Private Member Functions

virtual pathtprivate_peek ()=0
 
virtual void private_pop ()=0
 

Detailed Description

Storage for symbolic execution paths to be resumed later.

This data structure supports saving partially-executed symbolic execution paths so that their execution can be halted and resumed later. The choice of which path should be resumed next is implemented by subtypes of this abstract class.

Definition at line 24 of file path_storage.h.

Constructor & Destructor Documentation

◆ ~path_storaget()

virtual path_storaget::~path_storaget ( )
virtualdefault

Member Function Documentation

◆ empty()

bool path_storaget::empty ( ) const
inline

Is this storage empty?

Definition at line 75 of file path_storage.h.

References size().

Referenced by peek(), bmct::perform_symbolic_execution(), and pop().

◆ peek()

patht& path_storaget::peek ( )
inline

Reference to the next path to resume.

Definition at line 47 of file path_storage.h.

References empty(), PRECONDITION, and private_peek().

◆ pop()

void path_storaget::pop ( )
inline

Remove the next path to resume from the storage.

Definition at line 65 of file path_storage.h.

References empty(), PRECONDITION, and private_pop().

◆ private_peek()

virtual patht& path_storaget::private_peek ( )
privatepure virtual

Implemented in path_fifot, and path_lifot.

Referenced by peek().

◆ private_pop()

virtual void path_storaget::private_pop ( )
privatepure virtual

Implemented in path_fifot, and path_lifot.

Referenced by pop().

◆ push()

virtual void path_storaget::push ( const patht next_instruction,
const patht jump_target 
)
pure virtual

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

Implemented in path_fifot.

Referenced by goto_symext::symex_goto().

◆ size()

virtual std::size_t path_storaget::size ( ) const
pure virtual

How many paths does this storage contain?

Implemented in path_fifot, and path_lifot.

Referenced by empty().


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