cprover
|
Classes | |
struct | goalt |
struct | testt |
Public Types | |
typedef std::map< irep_idt, goalt > | goal_mapt |
typedef std::vector< testt > | testst |
Public Member Functions | |
bmc_covert (const goto_functionst &_goto_functions, bmct &_bmc) | |
bool | operator() () |
virtual void | satisfying_assignment () |
irep_idt | id (goto_programt::const_targett loc) |
std::string | get_test (const goto_tracet &goto_trace) const |
![]() | |
virtual void | goal_covered (const goalt &) |
Public Attributes | |
goal_mapt | goal_map |
testst | tests |
Protected Attributes | |
const goto_functionst & | goto_functions |
prop_convt & | solver |
bmct & | bmc |
Additional Inherited Members |
Definition at line 34 of file bmc_cover.cpp.
typedef std::map<irep_idt, goalt> bmc_covert::goal_mapt |
Definition at line 114 of file bmc_cover.cpp.
typedef std::vector<testt> bmc_covert::testst |
Definition at line 116 of file bmc_cover.cpp.
|
inline |
Definition at line 39 of file bmc_cover.cpp.
|
inline |
Definition at line 119 of file bmc_cover.cpp.
References bmc, from_expr(), id2string(), bmct::ns, and goto_tracet::steps.
Referenced by operator()().
|
inline |
bool bmc_covert::operator() | ( | void | ) |
Definition at line 193 of file bmc_cover.cpp.
References cover_goalst::add(), bmc, prop_convt::convert(), convert(), decision_proceduret::decision_procedure_text(), bmc_covert::goalt::description, bmct::do_conversion(), messaget::eom(), bmct::equation, forall_goto_functions, forall_goto_program_instructions, optionst::get_bool_option(), messaget::get_message_handler(), get_test(), goal_map, goto_functions, id(), id2string(), irept::is_not_nil(), cover_goalst::iterations(), json(), messaget::mstreamt::json_stream(), ui_message_handlert::JSON_UI, jsont::make_object(), xmlt::new_element(), bmct::ns, bmct::options, ui_message_handlert::PLAIN, json_arrayt::push_back(), json_stream_arrayt::push_back_stream_object(), cover_goalst::register_observer(), messaget::result(), bmc_covert::goalt::satisfied, xmlt::set_attribute(), messaget::set_message_handler(), cover_goalst::size(), solver, bmc_covert::goalt::source_location, symex_target_equationt::SSA_steps, messaget::statistics(), messaget::status(), tests, to_string(), bmct::trace_options(), bmct::ui, xml(), and ui_message_handlert::XML_UI.
|
virtual |
Reimplemented from cover_goalst::observert.
Definition at line 147 of file bmc_cover.cpp.
References bmc, build_goto_trace(), bmc_covert::testt::covered_goals, bmc_covert::goalt::description, messaget::eom(), bmct::equation, source_locationt::get_function(), goal_map, bmc_covert::testt::goto_trace, bmc_covert::goalt::instances, tvt::is_true(), prop_convt::l_get(), bmct::ns, bmc_covert::goalt::satisfied, solver, bmc_covert::goalt::source_location, symex_target_equationt::SSA_steps, messaget::status(), goto_tracet::steps, and tests.
|
protected |
Definition at line 144 of file bmc_cover.cpp.
Referenced by get_test(), operator()(), and satisfying_assignment().
goal_mapt bmc_covert::goal_map |
Definition at line 115 of file bmc_cover.cpp.
Referenced by operator()(), and satisfying_assignment().
|
protected |
Definition at line 142 of file bmc_cover.cpp.
Referenced by operator()().
|
protected |
Definition at line 143 of file bmc_cover.cpp.
Referenced by operator()(), and satisfying_assignment().
testst bmc_covert::tests |
Definition at line 117 of file bmc_cover.cpp.
Referenced by operator()(), and satisfying_assignment().