cprover
|
#include <bmc.h>
Public Member Functions | |
bmct (const optionst &_options, const symbol_tablet &_symbol_table, message_handlert &_message_handler, prop_convt &_prop_conv) | |
virtual resultt | run (const goto_functionst &goto_functions) |
virtual | ~bmct () |
void | set_ui (language_uit::uit _ui) |
virtual resultt | operator() (const goto_functionst &goto_functions) |
![]() | |
safety_checkert (const namespacet &_ns) | |
safety_checkert (const namespacet &_ns, message_handlert &_message_handler) | |
Public Attributes | |
expr_listt | bmc_constraints |
![]() | |
goto_tracet | error_trace |
Protected Member Functions | |
virtual decision_proceduret::resultt | run_decision_procedure (prop_convt &prop_conv) |
virtual resultt | decide (const goto_functionst &, prop_convt &) |
virtual void | setup_unwind () |
virtual void | do_unwind_module () |
void | do_conversion () |
virtual void | show_vcc () |
virtual void | show_vcc_plain (std::ostream &out) |
virtual void | show_vcc_json (std::ostream &out) |
virtual resultt | all_properties (const goto_functionst &goto_functions, prop_convt &solver) |
virtual resultt | stop_on_fail (const goto_functionst &goto_functions, prop_convt &solver) |
virtual void | show_program () |
virtual void | report_success () |
virtual void | report_failure () |
virtual void | error_trace () |
void | output_graphml (resultt result, const goto_functionst &goto_functions) |
outputs witnesses in graphml format More... | |
bool | cover (const goto_functionst &goto_functions, const optionst::value_listt &criteria) |
Try to cover all goals. More... | |
Protected Attributes | |
const optionst & | options |
symbol_tablet | new_symbol_table |
namespacet | ns |
symex_target_equationt | equation |
symex_bmct | symex |
prop_convt & | prop_conv |
language_uit::uit | ui |
![]() | |
const namespacet & | ns |
Friends | |
class | bmc_all_propertiest |
class | bmc_covert |
class | fault_localizationt |
Additional Inherited Members | |
![]() | |
enum | resultt { resultt::SAFE, resultt::UNSAFE, resultt::ERROR } |
|
inline |
Definition at line 35 of file bmc.h.
References goto_symext::constant_propagation, optionst::get_bool_option(), optionst::get_option(), options, symex_bmct::record_coverage, and symex.
|
protectedvirtual |
Definition at line 233 of file all_properties.cpp.
References messaget::get_message_handler(), and messaget::set_message_handler().
Referenced by decide().
|
protected |
Try to cover all goals.
Definition at line 435 of file bmc_cover.cpp.
References messaget::get_message_handler(), and messaget::set_message_handler().
Referenced by run().
|
protectedvirtual |
Definition at line 495 of file bmc.cpp.
References all_properties(), optionst::get_bool_option(), messaget::get_message_handler(), options, prop_conv, messaget::set_message_handler(), and stop_on_fail().
Referenced by run().
|
protected |
Definition at line 118 of file bmc.cpp.
References bmc_constraints, symex_target_equationt::convert(), do_unwind_module(), messaget::eom(), equation, forall_expr_list, prop_conv, decision_proceduret::set_to_true(), and messaget::status().
Referenced by bmc_all_propertiest::operator()(), bmc_covert::operator()(), run_decision_procedure(), and fault_localizationt::run_decision_procedure().
|
protectedvirtual |
Definition at line 46 of file bmc.cpp.
Referenced by do_conversion().
|
protectedvirtual |
Definition at line 51 of file bmc.cpp.
References build_goto_trace(), convert(), messaget::eom(), equation, safety_checkert::error_trace, id2string(), ui_message_handlert::JSON_UI, jsont::make_array(), jsont::make_object(), ns, goto_trace_stept::pc, ui_message_handlert::PLAIN, prop_conv, json_arrayt::push_back(), messaget::result(), show_goto_trace(), messaget::status(), goto_tracet::steps, ui, xml(), and ui_message_handlert::XML_UI.
Referenced by fault_localizationt::stop_on_fail(), and stop_on_fail().
|
inlinevirtual |
|
protected |
outputs witnesses in graphml format
Definition at line 93 of file bmc.cpp.
References equation, safety_checkert::error_trace, optionst::get_option(), graphml_witnesst::graph(), ns, options, messaget::result(), safety_checkert::SAFE, safety_checkert::UNSAFE, and write_graphml().
Referenced by run(), and stop_on_fail().
|
protectedvirtual |
Definition at line 193 of file bmc.cpp.
References xmlt::data, messaget::eom(), ui_message_handlert::JSON_UI, ui_message_handlert::PLAIN, messaget::result(), ui, xml(), and ui_message_handlert::XML_UI.
Referenced by bmc_all_propertiest::operator()(), fault_localizationt::stop_on_fail(), and stop_on_fail().
|
protectedvirtual |
Definition at line 165 of file bmc.cpp.
References xmlt::data, messaget::eom(), ui_message_handlert::JSON_UI, ui_message_handlert::PLAIN, messaget::result(), ui, xml(), and ui_message_handlert::XML_UI.
Referenced by bmc_all_propertiest::operator()(), run(), fault_localizationt::stop_on_fail(), and stop_on_fail().
|
virtual |
Definition at line 310 of file bmc.cpp.
References symex_target_equationt::count_ignored_SSA_steps(), cover(), CPROVER_PREFIX, decide(), messaget::eom(), equation, safety_checkert::ERROR, messaget::error(), optionst::get_bool_option(), optionst::get_list_option(), messaget::get_message_handler(), optionst::get_option(), symex_target_equationt::has_threads(), goto_symext::language_mode, symex_bmct::last_source_location, namespacet::lookup(), irept::make_nil(), symbolt::mode, ns, options, goto_symext::options, symex_bmct::output_coverage_report(), output_graphml(), prop_conv, goto_symext::remaining_vccs, report_success(), safety_checkert::SAFE, messaget::set_message_handler(), setup_unwind(), show_program(), show_vcc(), simple_slice(), slice(), symex_slice_by_tracet::slice_by_trace(), messaget::mstreamt::source_location, symex_target_equationt::SSA_steps, messaget::statistics(), messaget::status(), symex, and goto_symext::total_vccs.
Referenced by cbmc_parse_optionst::do_bmc(), instrumentert::is_cfg_spurious(), and operator()().
|
protectedvirtual |
Definition at line 139 of file bmc.cpp.
References current_time(), decision_proceduret::dec_solve(), decision_proceduret::decision_procedure_text(), do_conversion(), messaget::eom(), messaget::get_message_handler(), prop_conv, messaget::set_message_handler(), and messaget::status().
Referenced by stop_on_fail().
|
inline |
|
protectedvirtual |
Definition at line 543 of file bmc.cpp.
References optionst::get_option(), optionst::get_unsigned_int_option(), options, symex_bmct::set_unwind_limit(), symex_bmct::set_unwind_loop_limit(), symex_bmct::set_unwind_thread_loop_limit(), split_string(), symex, unsafe_string2int(), and unsafe_string2unsigned().
Referenced by run().
|
protectedvirtual |
Definition at line 221 of file bmc.cpp.
References equation, languagest::from_expr(), languages, new_ansi_c_language(), ns, and symex_target_equationt::SSA_steps.
Referenced by run().
|
protectedvirtual |
Definition at line 142 of file show_vcc.cpp.
References messaget::eom(), messaget::error(), optionst::get_option(), ui_message_handlert::JSON_UI, options, ui_message_handlert::PLAIN, show_vcc_json(), show_vcc_plain(), ui, and ui_message_handlert::XML_UI.
Referenced by run().
|
protectedvirtual |
Definition at line 84 of file show_vcc.cpp.
References equation, languagest::from_expr(), symex_target_equationt::has_threads(), irept::is_not_nil(), json(), languages, jsont::make_array(), jsont::make_object(), new_ansi_c_language(), ns, json_arrayt::push_back(), and symex_target_equationt::SSA_steps.
Referenced by show_vcc().
|
protectedvirtual |
Definition at line 26 of file show_vcc.cpp.
References equation, languagest::from_expr(), symex_target_equationt::has_threads(), languages, new_ansi_c_language(), ns, and symex_target_equationt::SSA_steps.
Referenced by show_vcc().
|
protectedvirtual |
Definition at line 507 of file bmc.cpp.
References decision_proceduret::D_SATISFIABLE, decision_proceduret::D_UNSATISFIABLE, messaget::eom(), equation, safety_checkert::ERROR, messaget::error(), error_trace(), optionst::get_bool_option(), optionst::get_option(), ns, options, output_graphml(), prop_conv, report_failure(), report_success(), run_decision_procedure(), safety_checkert::SAFE, and safety_checkert::UNSAFE.
Referenced by decide().
|
friend |
|
friend |
|
friend |
expr_listt bmct::bmc_constraints |
Definition at line 57 of file bmc.h.
Referenced by do_conversion().
|
protected |
Definition at line 72 of file bmc.h.
Referenced by fault_localizationt::collect_guards(), do_conversion(), error_trace(), fault_localizationt::freeze_guards(), fault_localizationt::get_failed_property(), bmc_all_propertiest::goal_covered(), fault_localizationt::goal_covered(), bmc_all_propertiest::operator()(), bmc_covert::operator()(), output_graphml(), run(), fault_localizationt::run(), bmc_covert::satisfying_assignment(), show_program(), show_vcc_json(), show_vcc_plain(), fault_localizationt::stop_on_fail(), and stop_on_fail().
|
protected |
|
protected |
Definition at line 71 of file bmc.h.
Referenced by error_trace(), bmc_covert::get_test(), bmc_all_propertiest::goal_covered(), fault_localizationt::goal_covered(), bmc_covert::operator()(), output_graphml(), bmc_all_propertiest::report(), run(), bmc_covert::satisfying_assignment(), show_program(), show_vcc_json(), show_vcc_plain(), fault_localizationt::stop_on_fail(), and stop_on_fail().
|
protected |
Definition at line 69 of file bmc.h.
Referenced by bmct(), decide(), bmc_covert::operator()(), output_graphml(), bmc_all_propertiest::report(), run(), setup_unwind(), show_vcc(), and stop_on_fail().
|
protected |
Definition at line 74 of file bmc.h.
Referenced by fault_localizationt::check(), decide(), do_conversion(), error_trace(), fault_localizationt::freeze_guards(), fault_localizationt::get_failed_property(), run(), fault_localizationt::run(), run_decision_procedure(), fault_localizationt::stop_on_fail(), stop_on_fail(), and fault_localizationt::update_scores().
|
protected |
Definition at line 73 of file bmc.h.
Referenced by bmct(), run(), and setup_unwind().
|
protected |
Definition at line 77 of file bmc.h.
Referenced by error_trace(), bmc_covert::operator()(), bmc_all_propertiest::report(), fault_localizationt::report(), report_failure(), report_success(), set_ui(), and show_vcc().