path_explorert Class Reference
Symbolic execution from a saved branch point. More...
#include <bmc.h>
Inheritance diagram for path_explorert:
Collaboration diagram for path_explorert:
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) | |
 Public Member Functions inherited from bmct | |
| 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) |
| Public Member Functions inherited from safety_checkert | |
| safety_checkert (const namespacet &_ns) | |
| safety_checkert (const namespacet &_ns, message_handlert &_message_handler) | |
| Public Member Functions inherited from messaget | |
Protected Attributes | |
| const goto_symex_statet & | saved_state |
| Protected Attributes inherited from bmct | |
| 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 |
| Protected Attributes inherited from safety_checkert | |
| const namespacet & | ns |
| Protected Attributes inherited from messaget | |
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 | |
| Public Types inherited from safety_checkert | |
| enum | resultt { resultt::SAFE, resultt::UNSAFE, resultt::ERROR, resultt::PAUSED, resultt::UNKNOWN } |
| Public Types inherited from messaget | |
| Static Public Member Functions inherited from bmct | |
| 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... | |
| Static Public Member Functions inherited from messaget | |
| Public Attributes inherited from safety_checkert | |
| goto_tracet | error_trace |
| Protected Member Functions inherited from bmct | |
| 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... | |
Detailed Description
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.
Constructor & Destructor Documentation
◆ path_explorert()
|
inline |
Member Function Documentation
◆ perform_symbolic_execution()
|
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.
Member Data Documentation
◆ saved_state
|
protected |
Definition at line 286 of file bmc.h.
Referenced by perform_symbolic_execution().
The documentation for this class was generated from the following files:
