CBMC
|
Return value for build_reference_to
; see that method for documentation.
More...
#include <value_set_dereference.h>
Public Member Functions | |
valuet () | |
Public Attributes | |
exprt | value |
exprt | pointer |
exprt | pointer_guard |
Return value for build_reference_to
; see that method for documentation.
Definition at line 58 of file value_set_dereference.h.
|
inline |
Definition at line 65 of file value_set_dereference.h.
exprt value_set_dereferencet::valuet::pointer |
Definition at line 62 of file value_set_dereference.h.
exprt value_set_dereferencet::valuet::pointer_guard |
Definition at line 63 of file value_set_dereference.h.
exprt value_set_dereferencet::valuet::value |
Definition at line 61 of file value_set_dereference.h.