12 #ifndef CPROVER_CBMC_BMC_H 13 #define CPROVER_CBMC_BMC_H 65 return run(goto_functions);
119 #endif // CPROVER_CBMC_BMC_H void output_graphml(resultt result, const goto_functionst &goto_functions)
outputs witnesses in graphml format
CNF Generation, via Tseitin.
Generate Equation using Symbolic Execution.
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)
bool constant_propagation
virtual void report_failure()
bool cover(const goto_functionst &goto_functions, const optionst::value_listt &criteria)
Try to cover all goals.
virtual void setup_unwind()
virtual resultt decide(const goto_functionst &, prop_convt &)
expr_listt bmc_constraints
virtual void error_trace()
virtual void do_unwind_module()
void set_ui(language_uit::uit _ui)
const std::string get_option(const std::string &option) const
bool get_bool_option(const std::string &option) const
std::list< std::string > value_listt
virtual resultt run(const goto_functionst &goto_functions)
virtual void show_vcc_json(std::ostream &out)
virtual decision_proceduret::resultt run_decision_procedure(prop_convt &prop_conv)
std::list< exprt > expr_listt
virtual resultt stop_on_fail(const goto_functionst &goto_functions, prop_convt &solver)
Safety Checker Interface.
bmct(const optionst &_options, const symbol_tablet &_symbol_table, message_handlert &_message_handler, prop_convt &_prop_conv)
virtual void show_program()
Bounded Model Checking for ANSI-C.
symbol_tablet new_symbol_table
symex_target_equationt equation
virtual void report_success()