12 #ifndef CPROVER_CBMC_BMC_H 13 #define CPROVER_CBMC_BMC_H 72 std::function<
bool(
void)> callback_after_symex)
105 return run(goto_functions);
126 std::function<
bool(
void)> callback_after_symex =
nullptr);
143 std::function<
bool(
void)> callback_after_symex)
162 "Should only use saved equation & goto_state constructor " 163 "when doing path exploration");
217 template <
template <
class goalt>
class covert>
259 std::function<
bool(
void)> callback_after_symex)
267 callback_after_symex),
290 "(unwinding-assertions)" \ 291 "(no-unwinding-assertions)" \ 292 "(no-pretty-names)" \ 293 "(no-self-loops-to-assumptions)" \ 296 "(show-symex-strategies)" \ 300 "(graphml-witness):" \ 304 " --paths [strategy] explore paths one at a time\n" \ 305 " --show-symex-strategies list strategies for use with --paths\n" \ 306 " --program-only only show program expression\n" \ 307 " --show-loops show the loops in the program\n" \ 308 " --depth nr limit search depth\n" \ 309 " --unwind nr unwind nr times\n" \ 310 " --unwindset L:B,... unwind loop L with a bound of B\n" \ 311 " (use --show-loops to get the loop IDs)\n" \ 312 " --show-vcc show the verification conditions\n" \ 313 " --slice-formula remove assignments unrelated to property\n" \ 314 " --unwinding-assertions generate unwinding assertions (cannot be\n" \ 315 " used with --cover or --partial-loops)\n" \ 316 " --partial-loops permit paths with partial loops\n" \ 317 " --no-self-loops-to-assumptions\n" \ 318 " do not simplify while(1){} to assume(0)\n" \ 319 " --no-pretty-names do not simplify identifiers\n" \ 320 " --graphml-witness filename write the witness in GraphML format to " \ 321 "filename\n" // NOLINT(*) 323 #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
bool cover(const goto_functionst &goto_functions)
Try to cover all goals.
Abstract interface to eager or lazy GOTO models.
ui_message_handlert & ui_message_handler
Generate Equation using Symbolic Execution.
const symbol_tablet & outer_symbol_table
symbol table for the goto-program that we will execute
virtual resultt all_properties(const goto_functionst &goto_functions, prop_convt &solver)
virtual resultt operator()(const goto_functionst &goto_functions)
path_storaget & path_storage
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
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 &)
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)
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.
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.
bool get_bool_option(const std::string &option) const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Symbolic execution from a saved branch point.
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.
A collection of goto functions.
Class that provides messages with a built-in verbosity 'level'.
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.
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)
Safety Checker Interface.
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).
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 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
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.
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.
void output_graphml(resultt result)
outputs witnesses in graphml format