|
CBMC
|
#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 |
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.