cprover
bmc_all_propertiest::goalt Struct Reference

#include <all_properties_class.h>

+ Collaboration diagram for bmc_all_propertiest::goalt:

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
 

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 46 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 64 of file all_properties_class.h.

◆ goalt() [2/2]

bmc_all_propertiest::goalt::goalt ( )
inline

Definition at line 72 of file all_properties_class.h.

Member Function Documentation

◆ as_expr()

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

Definition at line 76 of file all_properties_class.h.

◆ status_string()

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

Definition at line 49 of file all_properties_class.h.

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 47 of file all_properties_class.h.

◆ instances

instancest bmc_all_propertiest::goalt::instances

Definition at line 41 of file all_properties_class.h.

◆ source_location

source_locationt bmc_all_propertiest::goalt::source_location

Definition at line 43 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: