CBMC
|
#include <interpreter_class.h>
Public Types | |
enum class | initializedt { UNKNOWN , WRITTEN_BEFORE_READ , READ_BEFORE_WRITTEN } |
Public Member Functions | |
memory_cellt () | |
Public Attributes | |
mp_integer | value |
initializedt | initialized |
Definition at line 162 of file interpreter_class.h.
|
strong |
Enumerator | |
---|---|
UNKNOWN | |
WRITTEN_BEFORE_READ | |
READ_BEFORE_WRITTEN |
Definition at line 171 of file interpreter_class.h.
|
inline |
Definition at line 165 of file interpreter_class.h.
|
mutable |
Definition at line 178 of file interpreter_class.h.
mp_integer interpretert::memory_cellt::value |
Definition at line 169 of file interpreter_class.h.