cprover
|
Storage for symbolic execution paths to be resumed later. More...
#include <path_storage.h>
Classes | |
struct | patht |
Information saved at a conditional goto to resume execution. More... | |
Public Member Functions | |
virtual | ~path_storaget ()=default |
patht & | peek () |
Reference to the next path to resume. More... | |
virtual void | clear ()=0 |
Clear all saved paths. 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 patht & | private_peek ()=0 |
virtual void | private_pop ()=0 |
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.
|
virtualdefault |
|
pure virtual |
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.
Implemented in path_fifot, and path_lifot.
|
inline |
Is this storage empty?
Definition at line 83 of file path_storage.h.
References size().
Referenced by peek(), bmct::perform_symbolic_execution(), and pop().
|
inline |
Reference to the next path to resume.
Definition at line 47 of file path_storage.h.
References empty(), PRECONDITION, and private_peek().
|
inline |
Remove the next path to resume from the storage.
Definition at line 73 of file path_storage.h.
References empty(), PRECONDITION, and private_pop().
|
privatepure virtual |
Implemented in path_fifot, and path_lifot.
Referenced by peek().
|
privatepure virtual |
Implemented in path_fifot, and path_lifot.
Referenced by pop().
|
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.
next_instruction | the instruction following the goto instruction |
jump_target | the target instruction of the goto instruction |
Implemented in path_fifot.
Referenced by goto_symext::symex_goto().
|
pure virtual |
How many paths does this storage contain?
Implemented in path_fifot, and path_lifot.
Referenced by empty().