cprover
|
FIFO save queue: paths are resumed in the order that they were saved. More...
#include <path_storage.h>
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... | |
![]() | |
virtual | ~path_storaget ()=default |
patht & | peek () |
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< patht > | paths |
Private Member Functions | |
patht & | private_peek () override |
void | private_pop () override |
FIFO save queue: paths are resumed in the order that they were saved.
Definition at line 113 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 77 of file path_storage.cpp.
References paths.
|
overrideprivatevirtual |
|
overrideprivatevirtual |
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 |
Implements path_storaget.
Definition at line 59 of file path_storage.cpp.
References paths.
|
overridevirtual |
How many paths does this storage contain?
Implements path_storaget.
Definition at line 72 of file path_storage.cpp.
References paths.
|
protected |
Definition at line 121 of file path_storage.h.
Referenced by clear(), private_peek(), private_pop(), push(), and size().