CBMC
|
#include <solver_types.h>
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 |
Definition at line 165 of file solver_types.h.
using workt::patht = std::vector<frame_reft> |
Definition at line 167 of file solver_types.h.
|
inline |
Definition at line 169 of file solver_types.h.
frame_reft workt::frame |
Definition at line 177 of file solver_types.h.
exprt workt::invariant |
Definition at line 178 of file solver_types.h.
std::size_t workt::nondet_counter = 0 |
Definition at line 182 of file solver_types.h.
patht workt::path |
Definition at line 180 of file solver_types.h.