#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:

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

Classes

Public Types

Public Member Functions

Public Attributes