Go to the documentation of this file.
5 #ifndef CPROVER_GOTO_SYMEX_PATH_STORAGE_H
6 #define CPROVER_GOTO_SYMEX_PATH_STORAGE_H
59 virtual void clear() = 0;
80 virtual std::size_t
size()
const = 0;
100 std::size_t
size()
const override;
101 void clear()
override;
117 std::size_t
size()
const override;
118 void clear()
override;
147 std::unique_ptr<path_storaget>
get(
const std::string strategy)
const
151 found !=
strategies.end(),
"Unknown strategy '" + strategy +
"'.");
152 return found->second.second();
169 std::map<
const std::string,
170 std::pair<
const std::string,
171 const std::function<std::unique_ptr<path_storaget>()>>>
Class that provides messages with a built-in verbosity 'level'.
#define PRECONDITION(CONDITION)
std::unique_ptr< path_storaget > get(const std::string strategy) const
Factory for a path_storaget.
bool empty() const
Is this storage empty?
patht & private_peek() override
patht & peek()
Reference to the next path to resume.
patht(const symex_target_equationt &e, const goto_symex_statet &s)
FIFO save queue: paths are resumed in the order that they were saved.
void push(const patht &, const patht &) override
Add paths to resume to the storage.
Storage for symbolic execution paths to be resumed later.
std::map< const std::string, std::pair< const std::string, const std::function< std::unique_ptr< path_storaget >)> > > strategies
Map from the name of a strategy (to be supplied on the command line), to the help text for that strat...
virtual ~path_storaget()=default
void clear() override
Clear all saved paths.
void pop()
Remove the next path to resume from the storage.
void clear() override
Clear all saved paths.
void set_path_strategy_options(const cmdlinet &, optionst &, messaget &) const
add paths and exploration-strategy option, suitable to be invoked from front-ends.
symex_target_equationt equation
patht & private_peek() override
std::size_t size() const override
How many paths does this storage contain?
std::string show_strategies() const
suitable for displaying as a front-end help message
virtual void private_pop()=0
void private_pop() override
patht(const patht &other)
virtual void clear()=0
Clear all saved paths.
void push(const patht &, const patht &) override
Add paths to resume to the storage.
Information saved at a conditional goto to resume execution.
std::list< path_storaget::patht >::iterator last_peeked
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
std::string default_strategy() const
void private_pop() override
std::list< path_nodet > patht
bool is_valid_strategy(const std::string strategy) const
is there a factory constructor for the named strategy?
Factory and information for path_storaget.
std::size_t size() const override
How many paths does this storage contain?
virtual void push(const patht &next_instruction, const patht &jump_target)=0
Add paths to resume to the storage.
LIFO save queue: depth-first search, try to finish paths.
virtual std::size_t size() const =0
How many paths does this storage contain?
virtual patht & private_peek()=0