cprover
|
#include <all_properties_class.h>
Public Types | |
enum | statust { UNKNOWN, FAILURE, SUCCESS, ERROR } |
typedef std::vector< symex_target_equationt::SSA_stepst::iterator > | instancest |
Public Member Functions | |
std::string | status_string () const |
goalt (const goto_programt::instructiont &instruction) | |
goalt () | |
exprt | as_expr () const |
Public Attributes | |
instancest | instances |
std::string | description |
source_locationt | source_location |
enum bmc_all_propertiest::goalt::statust | status |
goto_tracet | goto_trace |
Definition at line 36 of file all_properties_class.h.
typedef std::vector<symex_target_equationt::SSA_stepst::iterator> bmc_all_propertiest::goalt::instancest |
Definition at line 40 of file all_properties_class.h.
Enumerator | |
---|---|
UNKNOWN | |
FAILURE | |
SUCCESS | |
ERROR |
Definition at line 46 of file all_properties_class.h.
|
inlineexplicit |
Definition at line 64 of file all_properties_class.h.
|
inline |
Definition at line 72 of file all_properties_class.h.
|
inline |
Definition at line 76 of file all_properties_class.h.
|
inline |
Definition at line 49 of file all_properties_class.h.
std::string bmc_all_propertiest::goalt::description |
Definition at line 42 of file all_properties_class.h.
goto_tracet bmc_all_propertiest::goalt::goto_trace |
Definition at line 47 of file all_properties_class.h.
instancest bmc_all_propertiest::goalt::instances |
Definition at line 41 of file all_properties_class.h.
source_locationt bmc_all_propertiest::goalt::source_location |
Definition at line 43 of file all_properties_class.h.
enum bmc_all_propertiest::goalt::statust bmc_all_propertiest::goalt::status |