CBMC
Classes | Public Types | Public Member Functions | Public Attributes | List of all members
propertyt Class Reference

#include <solver_types.h>

+ Collaboration diagram for propertyt:

Classes

struct  trace_statet
 
struct  trace_updatet
 

Public Types

using statust = enum { UNKNOWN, PASS, REFUTED, ERROR, DROPPED }
 
using tracet = std::vector< trace_statet >
 

Public Member Functions

 propertyt (source_locationt __source_location, frame_reft __frame, exprt __condition)
 
irep_idt property_id () const
 

Public Attributes

source_locationt source_location
 
frame_reft frame
 
exprt condition
 
statust status = UNKNOWN
 
std::chrono::time_point< std::chrono::steady_clock > start
 
std::chrono::time_point< std::chrono::steady_clock > stop
 
tracet trace
 

Detailed Description

Definition at line 115 of file solver_types.h.

Member Typedef Documentation

◆ statust

using propertyt::statust = enum { UNKNOWN, PASS, REFUTED, ERROR, DROPPED }

Definition at line 137 of file solver_types.h.

◆ tracet

using propertyt::tracet = std::vector<trace_statet>

Definition at line 157 of file solver_types.h.

Constructor & Destructor Documentation

◆ propertyt()

propertyt::propertyt ( source_locationt  __source_location,
frame_reft  __frame,
exprt  __condition 
)
inline

Definition at line 118 of file solver_types.h.

Member Function Documentation

◆ property_id()

irep_idt propertyt::property_id ( ) const
inline

Definition at line 128 of file solver_types.h.

Member Data Documentation

◆ condition

exprt propertyt::condition

Definition at line 135 of file solver_types.h.

◆ frame

frame_reft propertyt::frame

Definition at line 134 of file solver_types.h.

◆ source_location

source_locationt propertyt::source_location

Definition at line 133 of file solver_types.h.

◆ start

std::chrono::time_point<std::chrono::steady_clock> propertyt::start

Definition at line 139 of file solver_types.h.

◆ status

statust propertyt::status = UNKNOWN

Definition at line 138 of file solver_types.h.

◆ stop

std::chrono::time_point<std::chrono::steady_clock> propertyt::stop

Definition at line 139 of file solver_types.h.

◆ trace

tracet propertyt::trace

Definition at line 158 of file solver_types.h.

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