Go to the documentation of this file.
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
Class that provides messages with a built-in verbosity 'level'.
virtual resultt decide(const goto_functionst &, prop_convt &)
void perform_symbolic_execution(goto_symext::get_goto_functiont get_goto_function) override
Resume symbolic execution from saved branch point.
virtual resultt run(const goto_functionst &goto_functions)
trace_optionst trace_options()
Bounded model checking or path exploration for goto-programs.
virtual resultt operator()(const goto_functionst &goto_functions)
bool cover(const goto_functionst &goto_functions)
Try to cover all goals.
virtual void report_success()
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...
void output_graphml(resultt result)
outputs witnesses in graphml format
Storage for symbolic execution paths to be resumed later.
std::unique_ptr< memory_model_baset > memory_model
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.
void add_loop_unwind_handler(symex_bmct::loop_unwind_handlert handler)
void add_loop_unwind_handler(loop_unwind_handlert handler)
Add a callback function that will be called to determine whether to unwind loops.
virtual decision_proceduret::resultt run_decision_procedure(prop_convt &prop_conv)
path_storaget & path_storage
Storage of symbolic execution paths to resume.
virtual void error_trace()
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
ui_message_handlert & ui_message_handler
virtual void perform_symbolic_execution(goto_symext::get_goto_functiont get_goto_function)
Class-specific symbolic execution.
mstreamt & result() const
void add_unwind_recursion_handler(symex_bmct::recursion_unwind_handlert handler)
Symbolic execution from a saved branch point.
void add_recursion_unwind_handler(recursion_unwind_handlert handler)
Add a callback function that will be called to determine whether to unwind recursion.
virtual resultt stop_on_fail(prop_convt &solver)
safety_checkert::resultt execute(abstract_goto_modelt &)
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 ...
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)
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
const goto_symex_statet & saved_state
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).
A collection of goto functions.
std::function< bool(void)> driver_callback_after_symex
Optional callback, to be run after symex but before handing the resulting equation to the solver.
symbol_tablet symex_symbol_table
symbol table generated during symbolic execution
const symbol_tablet & outer_symbol_table
symbol table for the goto-program that we will execute
Class providing the abstract GOTO model interface onto an unrelated symbol table and goto_functionst.
int solver(std::istream &in)
bool get_bool_option(const std::string &option) const
virtual resultt all_properties(const goto_functionst &goto_functions, prop_convt &solver)
symex_target_equationt equation
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
Factory and information for path_storaget.
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.
virtual void report_failure()
virtual void freeze_program_variables()
Hook used by CEGIS to selectively freeze variables in the SAT solver after the SSA formula is added t...
Abstract interface to eager or lazy GOTO models.
friend class bmc_goal_covert