30 paths.push_back(next_instruction);
31 paths.push_back(jump_target);
58 paths.push_back(next_instruction);
59 paths.push_back(jump_target);
79 ss << pair.second.first;
88 if(cmdline.
isset(
"paths"))
91 std::string strategy = cmdline.
get_value(
"paths");
94 message.
error() <<
"Unknown strategy '" << strategy
95 <<
"'. Pass the --show-symex-strategies flag to list " 96 "available strategies." 100 options.
set_option(
"exploration-strategy", strategy);
109 {
" lifo next instruction is pushed before\n" 110 " goto target; paths are popped in\n" 111 " last-in, first-out order. Explores\n" 112 " the program tree depth-first.\n",
114 return util_make_unique<path_lifot>();
117 {
" fifo next instruction is pushed before\n" 118 " goto target; paths are popped in\n" 119 " first-in, first-out order. Explores\n" 120 " the program tree breadth-first.\n",
122 return util_make_unique<path_fifot>();
void private_pop() override
patht & private_peek() override
void push(const patht &, const patht &) override
Add paths to resume to the storage.
std::size_t size() const override
How many paths does this storage contain?
std::string get_value(char option) const
static mstreamt & eom(mstreamt &m)
std::string show_strategies() const
suitable for displaying as a front-end help message
virtual bool isset(char option) const
void set_path_strategy_options(const cmdlinet &, optionst &, messaget &) const
add paths and exploration-strategy option, suitable to be invoked from front-ends.
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?
#define PRECONDITION(CONDITION)
void private_pop() override
patht & private_peek() override
void push(const patht &, const patht &) override
Document and give macros for the exit codes of CPROVER binaries.
std::string default_strategy() const
Information saved at a conditional goto to resume execution.
void set_option(const std::string &option, const bool value)
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
Storage of symbolic execution paths to resume.
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...
std::list< path_storaget::patht >::iterator last_peeked