cprover
|
#include <fault_localization.h>
Classes | |
struct | lpointt |
Public Member Functions | |
fault_localizationt (const goto_functionst &_goto_functions, bmct &_bmc, const optionst &_options) | |
safety_checkert::resultt | operator() () |
safety_checkert::resultt | stop_on_fail () |
virtual void | goal_covered (const cover_goalst::goalt &) |
![]() | |
bmc_all_propertiest (const goto_functionst &_goto_functions, prop_convt &_solver, bmct &_bmc) | |
safety_checkert::resultt | operator() () |
![]() | |
virtual void | satisfying_assignment () |
Protected Types | |
typedef std::map< literalt, lpointt > | lpointst |
typedef std::map< irep_idt, lpointst > | lpoints_mapt |
typedef std::vector< tvt > | lpoints_valuet |
Protected Member Functions | |
void | run (irep_idt goal_id) |
void | collect_guards (lpointst &lpoints) |
void | freeze_guards () |
bool | check (const lpointst &lpoints, const lpoints_valuet &value) |
void | update_scores (lpointst &lpoints, const lpoints_valuet &value) |
void | localize_linear (lpointst &lpoints) |
symex_target_equationt::SSA_stepst::const_iterator | get_failed_property () |
decision_proceduret::resultt | run_decision_procedure (prop_convt &prop_conv) |
void | report (irep_idt goal_id) |
virtual void | report (const cover_goalst &cover_goals) |
virtual void | do_before_solving () |
Protected Attributes | |
const goto_functionst & | goto_functions |
bmct & | bmc |
const optionst & | options |
symex_target_equationt::SSA_stepst::const_iterator | failed |
lpoints_mapt | lpoints_map |
![]() | |
const goto_functionst & | goto_functions |
prop_convt & | solver |
bmct & | bmc |
Additional Inherited Members | |
![]() | |
typedef std::map< irep_idt, goalt > | goal_mapt |
![]() | |
goal_mapt | goal_map |
Definition at line 25 of file fault_localization.h.
|
protected |
Definition at line 63 of file fault_localization.h.
|
protected |
Definition at line 74 of file fault_localization.h.
|
protected |
Definition at line 62 of file fault_localization.h.
|
inlineexplicit |
Definition at line 29 of file fault_localization.h.
References bmc, messaget::get_message_handler(), and messaget::set_message_handler().
|
protected |
Definition at line 78 of file fault_localization.cpp.
References bmc, decision_proceduret::D_SATISFIABLE, failed, bmct::prop_conv, and prop_convt::set_assumptions().
Referenced by localize_linear().
|
protected |
Definition at line 40 of file fault_localization.cpp.
References bmc, bmct::equation, failed, symex_target_equationt::SSA_steps, and symex_targett::STATE.
Referenced by run().
|
inlineprotectedvirtual |
Reimplemented from bmc_all_propertiest.
Definition at line 97 of file fault_localization.h.
References freeze_guards().
|
protected |
Definition at line 28 of file fault_localization.cpp.
References bmc, bmct::equation, bmct::prop_conv, prop_convt::set_frozen(), and symex_target_equationt::SSA_steps.
Referenced by do_before_solving(), and run_decision_procedure().
|
protected |
Definition at line 64 of file fault_localization.cpp.
References bmc, bmct::equation, tvt::is_false(), tvt::is_true(), prop_convt::l_get(), bmct::prop_conv, and symex_target_equationt::SSA_steps.
Referenced by run().
|
virtual |
Reimplemented from bmc_all_propertiest.
Definition at line 266 of file fault_localization.cpp.
References bmc, build_goto_trace(), bmct::equation, bmc_all_propertiest::goal_map, tvt::is_false(), prop_convt::l_get(), bmct::ns, run(), and bmc_all_propertiest::solver.
|
protected |
Definition at line 121 of file fault_localization.cpp.
References check(), tvt::TV_FALSE, tvt::TV_TRUE, tvt::TV_UNKNOWN, and update_scores().
Referenced by run().
safety_checkert::resultt fault_localizationt::operator() | ( | void | ) |
Definition at line 195 of file fault_localization.cpp.
References optionst::get_bool_option(), bmc_all_propertiest::operator()(), options, and stop_on_fail().
|
protected |
Definition at line 166 of file fault_localization.cpp.
References messaget::debug(), messaget::eom(), failed, id2string(), lpoints_map, fault_localizationt::lpointt::score, messaget::mstreamt::source_location, messaget::status(), and fault_localizationt::lpointt::target.
Referenced by report(), and stop_on_fail().
|
protectedvirtual |
Reimplemented from bmc_all_propertiest.
Definition at line 297 of file fault_localization.cpp.
References bmc, messaget::eom(), bmc_all_propertiest::goal_map, ui_message_handlert::JSON_UI, cover_goalst::number_covered(), ui_message_handlert::PLAIN, report(), bmc_all_propertiest::report(), messaget::status(), bmct::ui, and ui_message_handlert::XML_UI.
|
protected |
Definition at line 139 of file fault_localization.cpp.
References bmc, collect_guards(), messaget::eom(), bmct::equation, failed, get_failed_property(), localize_linear(), lpoints_map, bmct::prop_conv, prop_convt::set_assumptions(), symex_target_equationt::SSA_steps, and messaget::status().
Referenced by goal_covered(), and stop_on_fail().
|
protected |
Definition at line 204 of file fault_localization.cpp.
References bmc, current_time(), decision_proceduret::dec_solve(), decision_proceduret::decision_procedure_text(), bmct::do_conversion(), messaget::eom(), freeze_guards(), messaget::get_message_handler(), messaget::set_message_handler(), and messaget::status().
Referenced by stop_on_fail().
safety_checkert::resultt fault_localizationt::stop_on_fail | ( | ) |
Definition at line 233 of file fault_localization.cpp.
References bmc, decision_proceduret::D_SATISFIABLE, decision_proceduret::D_UNSATISFIABLE, messaget::eom(), bmct::equation, safety_checkert::ERROR, messaget::error(), bmct::error_trace(), optionst::get_bool_option(), bmct::ns, options, bmct::prop_conv, report(), bmct::report_failure(), bmct::report_success(), run(), run_decision_procedure(), safety_checkert::SAFE, messaget::status(), and safety_checkert::UNSAFE.
Referenced by operator()().
|
protected |
Definition at line 104 of file fault_localization.cpp.
References bmc, tvt::is_false(), tvt::is_true(), prop_convt::l_get(), and bmct::prop_conv.
Referenced by localize_linear().
|
protected |
Definition at line 50 of file fault_localization.h.
Referenced by check(), collect_guards(), fault_localizationt(), freeze_guards(), get_failed_property(), goal_covered(), report(), run(), run_decision_procedure(), stop_on_fail(), and update_scores().
|
protected |
Definition at line 54 of file fault_localization.h.
Referenced by check(), collect_guards(), report(), and run().
|
protected |
Definition at line 49 of file fault_localization.h.
|
protected |
Definition at line 64 of file fault_localization.h.
|
protected |
Definition at line 51 of file fault_localization.h.
Referenced by operator()(), and stop_on_fail().