CBMC
workt Struct Reference

#include <solver_types.h>

+ Collaboration diagram for workt:

Public Types

using patht = std::vector< frame_reft >
 

Public Member Functions

 workt (frame_reft __frame, exprt __invariant, patht __path)
 

Public Attributes

frame_reft frame
 
exprt invariant
 
patht path
 
std::size_t nondet_counter = 0
 

Detailed Description

Definition at line 165 of file solver_types.h.

Member Typedef Documentation

◆ patht

using workt::patht = std::vector<frame_reft>

Definition at line 167 of file solver_types.h.

Constructor & Destructor Documentation

◆ workt()

workt::workt ( frame_reft  __frame,
exprt  __invariant,
patht  __path 
)
inline

Definition at line 169 of file solver_types.h.

Member Data Documentation

◆ frame

frame_reft workt::frame

Definition at line 177 of file solver_types.h.

◆ invariant

exprt workt::invariant

Definition at line 178 of file solver_types.h.

◆ nondet_counter

std::size_t workt::nondet_counter = 0

Definition at line 182 of file solver_types.h.

◆ path

patht workt::path

Definition at line 180 of file solver_types.h.


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