cprover
bmc_all_propertiest::goalt Struct Reference

#include <all_properties_class.h>

Collaboration diagram for bmc_all_propertiest::goalt:
[legend]

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
 
enum bmc_all_propertiest::goalt::statust status
 
goto_tracet goto_trace
 

Detailed Description

Definition at line 36 of file all_properties_class.h.

Member Typedef Documentation

§ instancest

typedef std::vector<symex_target_equationt::SSA_stepst::iterator> bmc_all_propertiest::goalt::instancest

Definition at line 40 of file all_properties_class.h.

Member Enumeration Documentation

§ statust

Enumerator
UNKNOWN 
FAILURE 
SUCCESS 
ERROR 

Definition at line 45 of file all_properties_class.h.

Constructor & Destructor Documentation

§ goalt() [1/2]

bmc_all_propertiest::goalt::goalt ( const goto_programt::instructiont &  instruction)
inlineexplicit

Definition at line 63 of file all_properties_class.h.

References id2string().

§ goalt() [2/2]

bmc_all_propertiest::goalt::goalt ( )
inline

Definition at line 70 of file all_properties_class.h.

Member Function Documentation

§ as_expr()

exprt bmc_all_propertiest::goalt::as_expr ( ) const
inline

Definition at line 74 of file all_properties_class.h.

References conjunction().

§ status_string()

std::string bmc_all_propertiest::goalt::status_string ( ) const
inline

Definition at line 48 of file all_properties_class.h.

References ERROR, FAILURE, SUCCESS, and UNKNOWN.

Member Data Documentation

§ description

std::string bmc_all_propertiest::goalt::description

Definition at line 42 of file all_properties_class.h.

§ goto_trace

goto_tracet bmc_all_propertiest::goalt::goto_trace

Definition at line 46 of file all_properties_class.h.

§ instances

instancest bmc_all_propertiest::goalt::instances

Definition at line 41 of file all_properties_class.h.

§ status

enum bmc_all_propertiest::goalt::statust bmc_all_propertiest::goalt::status

The documentation for this struct was generated from the following file: