cprover
|
#include <all_properties_class.h>
Classes | |
struct | goalt |
Public Types | |
typedef std::map< irep_idt, goalt > | goal_mapt |
Public Member Functions | |
bmc_all_propertiest (const goto_functionst &_goto_functions, prop_convt &_solver, bmct &_bmc) | |
safety_checkert::resultt | operator() () |
virtual void | goal_covered (const cover_goalst::goalt &) |
![]() | |
virtual void | satisfying_assignment () |
Public Attributes | |
goal_mapt | goal_map |
Protected Member Functions | |
virtual void | report (const cover_goalst &cover_goals) |
virtual void | do_before_solving () |
Protected Attributes | |
const goto_functionst & | goto_functions |
prop_convt & | solver |
bmct & | bmc |
Additional Inherited Members |
Definition at line 19 of file all_properties_class.h.
typedef std::map<irep_idt, goalt> bmc_all_propertiest::goal_mapt |
Definition at line 84 of file all_properties_class.h.
|
inline |
Definition at line 24 of file all_properties_class.h.
References goal_covered(), and operator()().
|
inlineprotectedvirtual |
Reimplemented in fault_localizationt.
Definition at line 93 of file all_properties_class.h.
Referenced by operator()().
|
virtual |
Reimplemented from cover_goalst::observert.
Reimplemented in fault_localizationt.
Definition at line 29 of file all_properties.cpp.
References bmc, build_goto_trace(), bmct::equation, goal_map, tvt::is_false(), prop_convt::l_get(), bmct::ns, and solver.
Referenced by bmc_all_propertiest().
safety_checkert::resultt bmc_all_propertiest::operator() | ( | void | ) |
Definition at line 55 of file all_properties.cpp.
References cover_goalst::add(), bmc, prop_convt::convert(), current_time(), decision_proceduret::D_ERROR, decision_proceduret::decision_procedure_text(), do_before_solving(), bmct::do_conversion(), messaget::eom(), bmct::equation, safety_checkert::ERROR, messaget::error(), forall_goto_functions, forall_goto_program_instructions, messaget::get_message_handler(), goal_map, goto_functions, id2string(), cover_goalst::number_covered(), cover_goalst::register_observer(), report(), bmct::report_failure(), bmct::report_success(), messaget::result(), safety_checkert::SAFE, messaget::set_message_handler(), solver, symex_target_equationt::SSA_steps, messaget::status(), and safety_checkert::UNSAFE.
Referenced by bmc_all_propertiest(), and fault_localizationt::operator()().
|
protectedvirtual |
Reimplemented in fault_localizationt.
Definition at line 160 of file all_properties.cpp.
References bmc, convert(), messaget::eom(), optionst::get_bool_option(), goal_map, id2string(), cover_goalst::iterations(), ui_message_handlert::JSON_UI, jsont::make_array(), jsont::make_object(), xmlt::new_element(), bmct::ns, cover_goalst::number_covered(), bmct::options, ui_message_handlert::PLAIN, json_arrayt::push_back(), messaget::result(), xmlt::set_attribute(), show_goto_trace(), cover_goalst::size(), messaget::status(), bmct::ui, and ui_message_handlert::XML_UI.
Referenced by operator()(), and fault_localizationt::report().
|
protected |
Definition at line 90 of file all_properties_class.h.
Referenced by goal_covered(), operator()(), and report().
goal_mapt bmc_all_propertiest::goal_map |
Definition at line 85 of file all_properties_class.h.
Referenced by goal_covered(), fault_localizationt::goal_covered(), operator()(), report(), and fault_localizationt::report().
|
protected |
Definition at line 88 of file all_properties_class.h.
Referenced by operator()().
|
protected |
Definition at line 89 of file all_properties_class.h.
Referenced by goal_covered(), fault_localizationt::goal_covered(), and operator()().