|
| | 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.
Inheritance diagram for path_explorert: