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 32 of file bmc_cover.cpp.
typedef std::map<irep_idt, goalt> bmc_covert::goal_mapt |
Definition at line 112 of file bmc_cover.cpp.
typedef std::vector<testt> bmc_covert::testst |
Definition at line 114 of file bmc_cover.cpp.
|
inline |
Definition at line 37 of file bmc_cover.cpp.
|
inline |
Definition at line 117 of file bmc_cover.cpp.
|
inline |
Definition at line 107 of file bmc_cover.cpp.
bool bmc_covert::operator() | ( | void | ) |
Definition at line 185 of file bmc_cover.cpp.
|
virtual |
Reimplemented from cover_goalst::observert.
Definition at line 152 of file bmc_cover.cpp.
|
protected |
Definition at line 142 of file bmc_cover.cpp.
goal_mapt bmc_covert::goal_map |
Definition at line 113 of file bmc_cover.cpp.
|
protected |
Definition at line 140 of file bmc_cover.cpp.
|
protected |
Definition at line 141 of file bmc_cover.cpp.
testst bmc_covert::tests |
Definition at line 115 of file bmc_cover.cpp.