|
| path_explorert (const optionst &_options, const symbol_tablet &outer_symbol_table, ui_message_handlert &_message_handler, prop_convt &_prop_conv, symex_target_equationt &saved_equation, const goto_symex_statet &saved_state, path_storaget &path_storage, std::function< bool(void)> callback_after_symex) |
|
| bmct (const optionst &_options, const symbol_tablet &outer_symbol_table, ui_message_handlert &_message_handler, prop_convt &_prop_conv, path_storaget &_path_storage, std::function< bool(void)> callback_after_symex) |
| Constructor for path exploration with freshly-initialized state. More...
|
|
virtual resultt | run (const goto_functionst &goto_functions) |
|
resultt | run (abstract_goto_modelt &) |
|
void | setup () |
|
safety_checkert::resultt | execute (abstract_goto_modelt &) |
|
virtual | ~bmct () |
|
virtual resultt | operator() (const goto_functionst &goto_functions) |
|
void | add_loop_unwind_handler (symex_bmct::loop_unwind_handlert handler) |
|
void | add_unwind_recursion_handler (symex_bmct::recursion_unwind_handlert handler) |
|
| safety_checkert (const namespacet &_ns) |
|
| safety_checkert (const namespacet &_ns, message_handlert &_message_handler) |
|
virtual void | set_message_handler (message_handlert &_message_handler) |
|
message_handlert & | get_message_handler () |
|
| messaget () |
|
| messaget (const messaget &other) |
|
messaget & | operator= (const messaget &other) |
|
| messaget (message_handlert &_message_handler) |
|
virtual | ~messaget () |
|
mstreamt & | get_mstream (unsigned message_level) const |
|
mstreamt & | error () const |
|
mstreamt & | warning () const |
|
mstreamt & | result () const |
|
mstreamt & | status () const |
|
mstreamt & | statistics () const |
|
mstreamt & | progress () const |
|
mstreamt & | debug () const |
|
void | conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const |
| Generate output to message_stream using output_generator if the configured verbosity is at least as high as that of message_stream . More...
|
|
|
enum | resultt { resultt::SAFE,
resultt::UNSAFE,
resultt::ERROR,
resultt::PAUSED
} |
|
enum | message_levelt {
M_ERROR =1,
M_WARNING =2,
M_RESULT =4,
M_STATUS =6,
M_STATISTICS =8,
M_PROGRESS =9,
M_DEBUG =10
} |
|
static int | do_language_agnostic_bmc (const path_strategy_choosert &path_strategy_chooser, const optionst &opts, abstract_goto_modelt &goto_model, ui_message_handlert &ui, std::function< void(bmct &, const symbol_tablet &)> driver_configure_bmc=nullptr, std::function< bool(void)> callback_after_symex=nullptr) |
| Perform core BMC, using an abstract model to supply GOTO function bodies (perhaps created on demand). More...
|
|
static unsigned | eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest) |
| Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More...
|
|
static commandt | command (unsigned c) |
| Create an ECMA-48 SGR (Select Graphic Rendition) command. More...
|
|
goto_tracet | error_trace |
|
static eomt | eom |
|
static const commandt | reset |
| return to default formatting, as defined by the terminal More...
|
|
static const commandt | red |
| render text with red foreground color More...
|
|
static const commandt | green |
| render text with green foreground color More...
|
|
static const commandt | yellow |
| render text with yellow foreground color More...
|
|
static const commandt | blue |
| render text with blue foreground color More...
|
|
static const commandt | magenta |
| render text with magenta foreground color More...
|
|
static const commandt | cyan |
| render text with cyan foreground color More...
|
|
static const commandt | bright_red |
| render text with bright red foreground color More...
|
|
static const commandt | bright_green |
| render text with bright green foreground color More...
|
|
static const commandt | bright_yellow |
| render text with bright yellow foreground color More...
|
|
static const commandt | bright_blue |
| render text with bright blue foreground color More...
|
|
static const commandt | bright_magenta |
| render text with bright magenta foreground color More...
|
|
static const commandt | bright_cyan |
| render text with bright cyan foreground color More...
|
|
static const commandt | bold |
| render text with bold font More...
|
|
static const commandt | faint |
| render text with faint font More...
|
|
static const commandt | italic |
| render italic text More...
|
|
static const commandt | underline |
| render underlined text More...
|
|
| bmct (const optionst &_options, const symbol_tablet &outer_symbol_table, ui_message_handlert &_message_handler, prop_convt &_prop_conv, symex_target_equationt &_equation, path_storaget &_path_storage, std::function< bool(void)> callback_after_symex) |
| Constructor for path exploration from saved state. More...
|
|
virtual decision_proceduret::resultt | run_decision_procedure (prop_convt &prop_conv) |
|
virtual resultt | decide (const goto_functionst &, prop_convt &) |
|
void | do_conversion () |
|
virtual void | freeze_program_variables () |
| Hook used by CEGIS to selectively freeze variables in the SAT solver after the SSA formula is added to the solver. More...
|
|
trace_optionst | trace_options () |
|
virtual resultt | all_properties (const goto_functionst &goto_functions, prop_convt &solver) |
|
virtual resultt | stop_on_fail (prop_convt &solver) |
|
virtual void | report_success () |
|
virtual void | report_failure () |
|
virtual void | error_trace () |
|
void | output_graphml (resultt result) |
| outputs witnesses in graphml format More...
|
|
void | get_memory_model () |
|
void | slice () |
|
void | show () |
|
bool | cover (const goto_functionst &goto_functions) |
| Try to cover all goals. More...
|
|
static void | report_success (messaget &, ui_message_handlert &) |
|
static void | report_failure (messaget &, ui_message_handlert &) |
|
Symbolic execution from a saved branch point.
Instances of this class execute a single program path from a saved branch point. The saved branch point is supplied to the constructor as a pair of goto_target_equationt (which holds the SSA steps executed so far), and a goto_symex_statet Note that the bmct base class can also execute a single path (it will do so if the --paths
flag is set in its options
member), but will always begin symbolic execution from the beginning of the program with fresh state.
Definition at line 248 of file bmc.h.