LIFO save queue: depth-first search, try to finish paths. More...
#include <path_storage.h>
Inheritance diagram for path_lifot: Collaboration diagram for path_lifot:Public Member Functions | |
| void | push (const patht &) override |
| Add a path 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... | |
| Public Member Functions inherited from path_storaget | |
| 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... | |
| std::size_t | get_unique_l1_index (const irep_idt &id, std::size_t minimum_index) |
Provide a unique L1 index for a given id, starting from minimum_index. More... | |
| std::size_t | get_unique_l2_index (const irep_idt &id) |
| void | add_function_loops (const irep_idt &identifier, const goto_programt &body) |
| Generates a loop analysis for the instructions in goto_programt and keys it against function ID. More... | |
| std::shared_ptr< lexical_loopst > | get_loop_analysis (const irep_idt &function_id) |
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 |
Additional Inherited Members | |
| Public Attributes inherited from path_storaget | |
| symex_nondet_generatort | build_symex_nondet |
| Counter for nondet objects, which require unique names. More... | |
| std::unordered_map< irep_idt, local_safe_pointerst > | safe_pointers |
| Map function identifiers to local_safe_pointerst instances. More... | |
| incremental_dirtyt | dirty |
| Local variables are considered 'dirty' if they've had an address taken and therefore may be referred to by a pointer. More... | |
Detailed Description
LIFO save queue: depth-first search, try to finish paths.
Definition at line 166 of file path_storage.h.
Member Function Documentation
◆ clear()
|
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 51 of file path_storage.cpp.
◆ private_peek()
|
overrideprivatevirtual |
Implements path_storaget.
Definition at line 27 of file path_storage.cpp.
◆ private_pop()
|
overrideprivatevirtual |
Implements path_storaget.
Definition at line 39 of file path_storage.cpp.
◆ push()
|
overridevirtual |
Add a path to resume to the storage.
Implements path_storaget.
Definition at line 34 of file path_storage.cpp.
◆ size()
|
overridevirtual |
How many paths does this storage contain?
Implements path_storaget.
Definition at line 46 of file path_storage.cpp.
Member Data Documentation
◆ last_peeked
|
protected |
Definition at line 174 of file path_storage.h.
◆ paths
|
protected |
Definition at line 175 of file path_storage.h.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/goto-symex/path_storage.h
- /home/runner/work/cbmc/cbmc/src/goto-symex/path_storage.cpp
