Storage of symbolic execution paths to resume. More...
#include <util/invariant.h>#include <analyses/dirty.h>#include <analyses/local_safe_pointers.h>#include "goto_symex_state.h"#include "symex_target_equation.h"#include <memory>
Include dependency graph for path_storage.h: This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Classes | |
| class | symex_nondet_generatort |
| Functor generating fresh nondet symbols. More... | |
| class | path_storaget |
| Storage for symbolic execution paths to be resumed later. More... | |
| struct | path_storaget::patht |
| Information saved at a conditional goto to resume execution. More... | |
| class | path_lifot |
| LIFO save queue: depth-first search, try to finish paths. More... | |
| class | path_fifot |
| FIFO save queue: paths are resumed in the order that they were saved. More... | |
Functions | |
| std::string | show_path_strategies () |
| suitable for displaying as a front-end help message More... | |
| bool | is_valid_path_strategy (const std::string strategy) |
| is there a factory constructor for the named strategy? More... | |
| std::unique_ptr< path_storaget > | get_path_strategy (const std::string strategy) |
| Ensure that is_valid_strategy() returns true for a particular string before calling this function on that string. More... | |
| void | parse_path_strategy_options (const cmdlinet &, optionst &, message_handlert &) |
add paths and exploration-strategy option, suitable to be invoked from front-ends. More... | |
Detailed Description
Storage of symbolic execution paths to resume.
Definition in file path_storage.h.
Function Documentation
◆ get_path_strategy()
| std::unique_ptr<path_storaget> get_path_strategy | ( | const std::string | strategy | ) |
Ensure that is_valid_strategy() returns true for a particular string before calling this function on that string.
Definition at line 128 of file path_storage.cpp.
◆ is_valid_path_strategy()
| bool is_valid_path_strategy | ( | const std::string | strategy | ) |
is there a factory constructor for the named strategy?
Definition at line 123 of file path_storage.cpp.
◆ parse_path_strategy_options()
| void parse_path_strategy_options | ( | const cmdlinet & | cmdline, |
| optionst & | options, | ||
| message_handlert & | message_handler | ||
| ) |
add paths and exploration-strategy option, suitable to be invoked from front-ends.
Definition at line 136 of file path_storage.cpp.
◆ show_path_strategies()
| std::string show_path_strategies | ( | ) |
suitable for displaying as a front-end help message
Definition at line 110 of file path_storage.cpp.
