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

enum bmc_all_propertiest::goalt::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:

• cbmc/all_properties_class.h