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 description, and 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(), and instances.

◆ 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, status, SUCCESS, and UNKNOWN.

Member Data Documentation

◆ description

std::string bmc_all_propertiest::goalt::description

Definition at line 42 of file all_properties_class.h.

Referenced by goalt().

◆ 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.

Referenced by as_expr().

◆ status

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

Referenced by status_string().


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