Storage for symbolic execution paths to be resumed later.
More...
#include <path_storage.h>
|
struct | patht |
| Information saved at a conditional goto to resume execution. More...
|
|
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.
◆ ~path_storaget()
virtual path_storaget::~path_storaget |
( |
| ) |
|
|
virtualdefault |
◆ clear()
virtual void path_storaget::clear |
( |
| ) |
|
|
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.
◆ empty()
bool path_storaget::empty |
( |
| ) |
const |
|
inline |
◆ peek()
patht& path_storaget::peek |
( |
| ) |
|
|
inline |
Reference to the next path to resume.
Definition at line 47 of file path_storage.h.
◆ pop()
void path_storaget::pop |
( |
| ) |
|
|
inline |
Remove the next path to resume from the storage.
Definition at line 73 of file path_storage.h.
◆ private_peek()
virtual patht& path_storaget::private_peek |
( |
| ) |
|
|
privatepure virtual |
◆ private_pop()
virtual void path_storaget::private_pop |
( |
| ) |
|
|
privatepure virtual |
◆ 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_instruction | the instruction following the goto instruction |
jump_target | the target instruction of the goto instruction |
Implemented in path_fifot, and path_lifot.
◆ size()
virtual std::size_t path_storaget::size |
( |
| ) |
const |
|
pure virtual |
The documentation for this class was generated from the following file: