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 35 of file bmc_cover.cpp.
typedef std::map<irep_idt, goalt> bmc_covert::goal_mapt |
Definition at line 115 of file bmc_cover.cpp.
typedef std::vector<testt> bmc_covert::testst |
Definition at line 117 of file bmc_cover.cpp.
|
inline |
Definition at line 40 of file bmc_cover.cpp.
|
inline |
Definition at line 120 of file bmc_cover.cpp.
|
inline |
Definition at line 110 of file bmc_cover.cpp.
bool bmc_covert::operator() | ( | void | ) |
Definition at line 188 of file bmc_cover.cpp.
|
virtual |
Reimplemented from cover_goalst::observert.
Definition at line 155 of file bmc_cover.cpp.
|
protected |
Definition at line 145 of file bmc_cover.cpp.
goal_mapt bmc_covert::goal_map |
Definition at line 116 of file bmc_cover.cpp.
|
protected |
Definition at line 143 of file bmc_cover.cpp.
|
protected |
Definition at line 144 of file bmc_cover.cpp.
testst bmc_covert::tests |
Definition at line 118 of file bmc_cover.cpp.