Go to the documentation of this file.
30 paths.push_back(next_instruction);
31 paths.push_back(jump_target);
63 paths.push_back(next_instruction);
64 paths.push_back(jump_target);
89 ss << pair.second.first;
98 if(cmdline.
isset(
"paths"))
101 std::string strategy = cmdline.
get_value(
"paths");
104 message.
error() <<
"Unknown strategy '" << strategy
105 <<
"'. Pass the --show-symex-strategies flag to list "
106 "available strategies."
110 options.
set_option(
"exploration-strategy", strategy);
119 {
" lifo next instruction is pushed before\n"
120 " goto target; paths are popped in\n"
121 " last-in, first-out order. Explores\n"
122 " the program tree depth-first.\n",
124 return util_make_unique<path_lifot>();
127 {
" fifo next instruction is pushed before\n"
128 " goto target; paths are popped in\n"
129 " first-in, first-out order. Explores\n"
130 " the program tree breadth-first.\n",
132 return util_make_unique<path_fifot>();
Class that provides messages with a built-in verbosity 'level'.
#define PRECONDITION(CONDITION)
patht & private_peek() override
virtual bool isset(char option) const
void push(const patht &, const patht &) override
Add paths to resume to the storage.
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...
void set_option(const std::string &option, const bool value)
void clear() override
Clear all saved paths.
void clear() override
Clear all saved paths.
Storage of symbolic execution paths to resume.
void set_path_strategy_options(const cmdlinet &, optionst &, messaget &) const
add paths and exploration-strategy option, suitable to be invoked from front-ends.
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
std::string get_value(char option) const
void private_pop() override
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
std::string default_strategy() const
void private_pop() override
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
bool is_valid_strategy(const std::string strategy) const
is there a factory constructor for the named strategy?
std::size_t size() const override
How many paths does this storage contain?