cprover
|
Classes | |
struct | instancet |
Public Types | |
typedef std::vector< instancet > | instancest |
Public Member Functions | |
void | add_instance (symex_target_equationt::SSA_stepst::iterator step, literalt condition) |
goalt (const std::string &_description, const source_locationt &_source_location) | |
goalt () | |
exprt | as_expr () const |
Public Attributes | |
instancest | instances |
std::string | description |
source_locationt | source_location |
bool | satisfied |
Definition at line 48 of file bmc_cover.cpp.
typedef std::vector<instancet> bmc_covert::goalt::instancest |
Definition at line 57 of file bmc_cover.cpp.
|
inline |
Definition at line 75 of file bmc_cover.cpp.
|
inline |
Definition at line 84 of file bmc_cover.cpp.
|
inline |
Definition at line 60 of file bmc_cover.cpp.
References instances.
|
inline |
Definition at line 89 of file bmc_cover.cpp.
References disjunction(), and instances.
std::string bmc_covert::goalt::description |
Definition at line 69 of file bmc_cover.cpp.
Referenced by bmc_covert::operator()(), and bmc_covert::satisfying_assignment().
instancest bmc_covert::goalt::instances |
Definition at line 58 of file bmc_cover.cpp.
Referenced by add_instance(), as_expr(), and bmc_covert::satisfying_assignment().
bool bmc_covert::goalt::satisfied |
Definition at line 73 of file bmc_cover.cpp.
Referenced by bmc_covert::operator()(), and bmc_covert::satisfying_assignment().
source_locationt bmc_covert::goalt::source_location |
Definition at line 70 of file bmc_cover.cpp.
Referenced by bmc_covert::operator()().