12 #ifndef CPROVER_CBMC_BMC_H 13 #define CPROVER_CBMC_BMC_H 72 std::function<
bool(
void)> callback_after_symex)
112 return run(goto_functions);
133 driver_configure_bmc =
nullptr,
134 std::function<
bool(
void)> callback_after_symex =
nullptr);
151 std::function<
bool(
void)> callback_after_symex)
173 "Should only use saved equation & goto_state constructor " 174 "when doing path exploration");
230 template <
template <
class goalt>
class covert>
272 std::function<
bool(
void)> callback_after_symex)
280 callback_after_symex),
302 "(unwinding-assertions)" \ 303 "(no-unwinding-assertions)" \ 304 "(no-pretty-names)" \ 305 "(no-self-loops-to-assumptions)" \ 308 "(show-symex-strategies)" \ 312 "(graphml-witness):" \ 316 " --paths [strategy] explore paths one at a time\n" \ 317 " --show-symex-strategies list strategies for use with --paths\n" \ 318 " --program-only only show program expression\n" \ 319 " --show-loops show the loops in the program\n" \ 320 " --depth nr limit search depth\n" \ 321 " --unwind nr unwind nr times\n" \ 322 " --unwindset L:B,... unwind loop L with a bound of B\n" \ 323 " (use --show-loops to get the loop IDs)\n" \ 324 " --show-vcc show the verification conditions\n" \ 325 " --slice-formula remove assignments unrelated to property\n" \ 326 " --unwinding-assertions generate unwinding assertions (cannot be\n" \ 327 " used with --cover or --partial-loops)\n" \ 328 " --partial-loops permit paths with partial loops\n" \ 329 " --no-self-loops-to-assumptions\n" \ 330 " do not simplify while(1){} to assume(0)\n" \ 331 " --no-pretty-names do not simplify identifiers\n" \ 332 " --graphml-witness filename write the witness in GraphML format to " \ 333 "filename\n" // NOLINT(*) 336 #endif // CPROVER_CBMC_BMC_H
virtual void perform_symbolic_execution(goto_symext::get_goto_functiont get_goto_function)
Class-specific symbolic execution.
friend class bmc_goal_covert
void set_ui(ui_message_handlert::uit _ui)
bool cover(const goto_functionst &goto_functions)
Try to cover all goals.
Abstract interface to eager or lazy GOTO models.
Generate Equation using Symbolic Execution.
const symbol_tablet & outer_symbol_table
symbol table for the goto-program that we will execute
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.
virtual void show_vcc_plain(std::ostream &out)
virtual resultt all_properties(const goto_functionst &goto_functions, prop_convt &solver)
virtual resultt operator()(const goto_functionst &goto_functions)
path_storaget & path_storage
bool constant_propagation
virtual void report_failure()
Decision Procedure Interface.
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
virtual resultt decide(const goto_functionst &, prop_convt &)
#define INVARIANT(CONDITION, REASON)
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)...
Factory and information for path_storaget.
void add_loop_unwind_handler(loop_unwind_handlert handler)
Add a callback function that will be called to determine whether to unwind loops. ...
const goto_symex_statet & saved_state
void add_unwind_recursion_handler(symex_bmct::recursion_unwind_handlert handler)
bool self_loops_to_assumptions
void add_loop_unwind_handler(symex_bmct::loop_unwind_handlert handler)
virtual void error_trace()
void add_recursion_unwind_handler(recursion_unwind_handlert handler)
Add a callback function that will be called to determine whether to unwind recursion.
ui_message_handlert::uit ui
int solver(std::istream &in)
void perform_symbolic_execution(goto_symext::get_goto_functiont get_goto_function) override
Resume symbolic execution from saved branch point.
const std::string get_option(const std::string &option) const
bool get_bool_option(const std::string &option) const
Symbolic execution from a saved branch point.
virtual void show_vcc_json(std::ostream &out)
std::function< tvt(const goto_symex_statet::call_stackt &, unsigned, unsigned, unsigned &)> loop_unwind_handlert
Loop unwind handlers take the call stack, loop number, the unwind count so far, and an out-parameter ...
virtual decision_proceduret::resultt run_decision_procedure(prop_convt &prop_conv)
Storage for symbolic execution paths to be resumed later.
Safety Checker Interface.
mstreamt & result() const
Memory models for partial order concurrency.
safety_checkert::resultt execute(abstract_goto_modelt &)
virtual resultt run(const goto_functionst &goto_functions)
virtual void show_program()
virtual resultt stop_on_fail(prop_convt &solver)
Bounded Model Checking for ANSI-C.
Class providing the abstract GOTO model interface onto an unrelated symbol table and goto_functionst...
symbol_tablet symex_symbol_table
symbol table generated during symbolic execution
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.
Bounded model checking or path exploration for goto-programs.
std::unique_ptr< memory_model_baset > memory_model
symex_target_equationt equation
std::function< bool(void)> driver_callback_after_symex
Optional callback, to be run after symex but before handing the resulting equation to the solver...
virtual void report_success()
trace_optionst trace_options()
virtual void freeze_program_variables()
Hook used by CEGIS to selectively freeze variables in the SAT solver after the SSA formula is added t...
std::function< tvt(const irep_idt &, unsigned, unsigned &)> recursion_unwind_handlert
Recursion unwind handlers take the function ID, the unwind count so far, and an out-parameter specify...
Storage of symbolic execution paths to resume.
void output_graphml(resultt result)
outputs witnesses in graphml format
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)