cprover
|
API to expression classes for Pointers. More...
#include "std_expr.h"
Go to the source code of this file.
Classes | |
class | object_descriptor_exprt |
Split an expression into a base object and a (byte) offset. More... | |
class | dynamic_object_exprt |
Representation of heap-allocated objects. More... | |
class | is_dynamic_object_exprt |
Evaluates to true if the operand is a pointer to a dynamic object. More... | |
class | address_of_exprt |
Operator to return the address of an object. More... | |
class | dereference_exprt |
Operator to dereference a pointer. More... | |
API to expression classes for Pointers.
Definition in file pointer_expr.h.
|
inline |
Definition at line 221 of file pointer_expr.h.
|
inline |
Definition at line 296 of file pointer_expr.h.
|
inline |
Definition at line 135 of file pointer_expr.h.
|
inline |
Definition at line 71 of file pointer_expr.h.
|
inline |
Cast an exprt to an address_of_exprt.
expr must be known to be address_of_exprt.
expr | Source expression |
Definition at line 237 of file pointer_expr.h.
|
inline |
Cast an exprt to an address_of_exprt.
expr must be known to be address_of_exprt.
expr | Source expression |
Definition at line 246 of file pointer_expr.h.
|
inline |
Cast an exprt to a dereference_exprt.
expr must be known to be dereference_exprt.
expr | Source expression |
Definition at line 312 of file pointer_expr.h.
|
inline |
Cast an exprt to a dereference_exprt.
expr must be known to be dereference_exprt.
expr | Source expression |
Definition at line 321 of file pointer_expr.h.
|
inline |
Cast an exprt to a dynamic_object_exprt.
expr must be known to be dynamic_object_exprt.
expr | Source expression |
Definition at line 151 of file pointer_expr.h.
|
inline |
Cast an exprt to a dynamic_object_exprt.
expr must be known to be dynamic_object_exprt.
expr | Source expression |
Definition at line 161 of file pointer_expr.h.
|
inline |
Definition at line 180 of file pointer_expr.h.
|
inline |
Definition at line 190 of file pointer_expr.h.
|
inline |
Cast an exprt to an object_descriptor_exprt.
expr must be known to be object_descriptor_exprt.
expr | Source expression |
Definition at line 88 of file pointer_expr.h.
|
inline |
Cast an exprt to an object_descriptor_exprt.
expr must be known to be object_descriptor_exprt.
expr | Source expression |
Definition at line 98 of file pointer_expr.h.
|
inline |
Definition at line 226 of file pointer_expr.h.
|
inline |
Definition at line 301 of file pointer_expr.h.
|
inline |
Definition at line 140 of file pointer_expr.h.
|
inline |
Definition at line 76 of file pointer_expr.h.