cprover
|
Symbolic execution from a saved branch point. More...
#include <bmc.h>
Public Member Functions | |
path_explorert (const optionst &_options, const symbol_tablet &outer_symbol_table, 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, 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 () |
void | set_ui (ui_message_handlert::uit _ui) |
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) | |
Protected Attributes | |
const goto_symex_statet & | saved_state |
![]() | |
const optionst & | options |
const symbol_tablet & | outer_symbol_table |
symbol table for the goto-program that we will execute More... | |
symbol_tablet | symex_symbol_table |
symbol table generated during symbolic execution More... | |
namespacet | ns |
symex_target_equationt | equation |
path_storaget & | path_storage |
symex_bmct | symex |
prop_convt & | prop_conv |
std::unique_ptr< memory_model_baset > | memory_model |
ui_message_handlert::uit | ui |
![]() | |
const namespacet & | ns |
Private Member Functions | |
void | perform_symbolic_execution (goto_symext::get_goto_functiont get_goto_function) override |
Resume symbolic execution from saved branch point. More... | |
Additional Inherited Members | |
![]() | |
enum | resultt { resultt::SAFE, resultt::UNSAFE, resultt::ERROR, resultt::PAUSED, resultt::UNKNOWN } |
![]() | |
static int | do_language_agnostic_bmc (const path_strategy_choosert &path_strategy_chooser, const optionst &opts, abstract_goto_modelt &goto_model, const ui_message_handlert::uit &ui, messaget &message, 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... | |
![]() | |
goto_tracet | error_trace |
![]() | |
bmct (const optionst &_options, const symbol_tablet &outer_symbol_table, 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... | |
virtual void | show_vcc () |
virtual void | show_vcc_plain (std::ostream &out) |
virtual void | show_vcc_json (std::ostream &out) |
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 | show_program () |
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... | |
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.
|
inline |
|
overrideprivatevirtual |
Resume symbolic execution from saved branch point.
This overrides the base implementation to call the symbolic executor with the saved symex_target_equationt, symbol_tablet, and goto_symex_statet provided as arguments to the constructor of this class.
Reimplemented from bmct.
Definition at line 705 of file bmc.cpp.
References bmct::equation, goto_symext::resume_symex_from_saved_state(), saved_state, bmct::symex, and bmct::symex_symbol_table.
|
protected |
Definition at line 286 of file bmc.h.
Referenced by perform_symbolic_execution().