Loading...

Searching...

No Matches

Classes | Public Types | Public Member Functions | Public Attributes | List of all members

propertyt Class Reference

#include <solver_types.h>

+ Collaboration diagram for propertyt:

[フレーム]

[legend]

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:

/home/runner/work/cbmc/cbmc/src/cprover/solver_types.h