cprover
|
LIFO save queue: depth-first search, try to finish paths. More...
#include <path_storage.h>
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... | |
![]() | |
virtual | ~path_storaget ()=default |
patht & | peek () |
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< patht > | paths |
Private Member Functions | |
patht & | private_peek () override |
void | private_pop () override |
LIFO save queue: depth-first search, try to finish paths.
Definition at line 96 of file path_storage.h.
|
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.
|
overrideprivatevirtual |
Implements path_storaget.
Definition at line 19 of file path_storage.cpp.
References last_peeked, and paths.
|
overrideprivatevirtual |
Implements path_storaget.
Definition at line 34 of file path_storage.cpp.
References last_peeked, paths, and PRECONDITION.
Definition at line 26 of file path_storage.cpp.
References paths.
|
overridevirtual |
How many paths does this storage contain?
Implements path_storaget.
Definition at line 41 of file path_storage.cpp.
References paths.
|
protected |
Definition at line 104 of file path_storage.h.
Referenced by private_peek(), and private_pop().
|
protected |
Definition at line 105 of file path_storage.h.
Referenced by clear(), private_peek(), private_pop(), push(), and size().