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... | |
![]() | |
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 104 of file path_storage.h.
|
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 54 of file path_storage.cpp.
References paths.
|
overridevirtual |
How many paths does this storage contain?
Implements path_storaget.
Definition at line 67 of file path_storage.cpp.
References paths.
|
protected |
Definition at line 111 of file path_storage.h.
Referenced by private_peek(), private_pop(), push(), and size().