cprover
|
API to expression classes for Pointers. More...
Go to the source code of this file.
Classes | |
class | pointer_typet |
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they have a subtype) More... | |
class | reference_typet |
The reference type. More... | |
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 | object_address_exprt |
Operator to return the address of an object. More... | |
class | field_address_exprt |
Operator to return the address of a field relative to a base address. More... | |
class | element_address_exprt |
Operator to return the address of an array element relative to a base address. More... | |
class | dereference_exprt |
Operator to dereference a pointer. More... | |
class | null_pointer_exprt |
The null pointer constant. More... | |
class | r_or_w_ok_exprt |
A base class for a predicate that indicates that an address range is ok to read or write or both. More... | |
class | r_ok_exprt |
A predicate that indicates that an address range is ok to read. More... | |
class | w_ok_exprt |
A predicate that indicates that an address range is ok to write. More... | |
API to expression classes for Pointers.
Definition in file pointer_expr.h.
|
inline |
Definition at line 362 of file pointer_expr.h.
|
inline |
Definition at line 668 of file pointer_expr.h.
|
inline |
Definition at line 265 of file pointer_expr.h.
|
inline |
Definition at line 592 of file pointer_expr.h.
|
inline |
Definition at line 510 of file pointer_expr.h.
|
inline |
Definition at line 310 of file pointer_expr.h.
|
inline |
Definition at line 426 of file pointer_expr.h.
|
inline |
Definition at line 201 of file pointer_expr.h.
|
inline |
Check whether a reference to a typet is a pointer_typet.
type | Source type. |
type
is a pointer_typet. Definition at line 49 of file pointer_expr.h.
|
inline |
Check whether a reference to a typet is a reference_typet.
type | Source type. |
type
is a reference_typet. Definition at line 115 of file pointer_expr.h.
bool is_reference | ( | const typet & | type | ) |
Returns true if the type is a reference.
Definition at line 129 of file std_types.cpp.
bool is_rvalue_reference | ( | const typet & | type | ) |
Returns if the type is an R value reference.
Definition at line 136 of file std_types.cpp.
|
inline |
This method tests, if the given typet is a pointer of type void.
Definition at line 79 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 378 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 387 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 684 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 693 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 281 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 291 of file pointer_expr.h.
|
inline |
Cast an exprt to an element_address_exprt.
expr must be known to be element_address_exprt.
expr | Source expression |
Definition at line 608 of file pointer_expr.h.
|
inline |
Cast an exprt to an element_address_exprt.
expr must be known to be element_address_exprt.
expr | Source expression |
Definition at line 618 of file pointer_expr.h.
|
inline |
Cast an exprt to an field_address_exprt.
expr must be known to be field_address_exprt.
expr | Source expression |
Definition at line 526 of file pointer_expr.h.
|
inline |
Cast an exprt to an field_address_exprt.
expr must be known to be field_address_exprt.
expr | Source expression |
Definition at line 536 of file pointer_expr.h.
|
inline |
Definition at line 321 of file pointer_expr.h.
|
inline |
Definition at line 331 of file pointer_expr.h.
|
inline |
Cast an exprt to an object_address_exprt.
expr must be known to be object_address_exprt.
expr | Source expression |
Definition at line 442 of file pointer_expr.h.
|
inline |
Cast an exprt to an object_address_exprt.
expr must be known to be object_address_exprt.
expr | Source expression |
Definition at line 452 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 218 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 228 of file pointer_expr.h.
|
inline |
Cast a typet to a pointer_typet.
This is an unchecked conversion. type must be known to be pointer_typet. Will fail with a precondition violation if type doesn't match.
type | Source type. |
Definition at line 62 of file pointer_expr.h.
|
inline |
Cast a typet to a pointer_typet.
This is an unchecked conversion. type must be known to be pointer_typet. Will fail with a precondition violation if type doesn't match.
type | Source type. |
Definition at line 70 of file pointer_expr.h.
|
inline |
Definition at line 751 of file pointer_expr.h.
|
inline |
Definition at line 732 of file pointer_expr.h.
|
inline |
Cast a typet to a reference_typet.
This is an unchecked conversion. type must be known to be reference_typet. Will fail with a precondition violation if type doesn't match.
type | Source type. |
Definition at line 128 of file pointer_expr.h.
|
inline |
Cast a typet to a reference_typet.
This is an unchecked conversion. type must be known to be reference_typet. Will fail with a precondition violation if type doesn't match.
type | Source type. |
Definition at line 135 of file pointer_expr.h.
|
inline |
Definition at line 769 of file pointer_expr.h.
|
inline |
Definition at line 367 of file pointer_expr.h.
|
inline |
Definition at line 673 of file pointer_expr.h.
|
inline |
Definition at line 270 of file pointer_expr.h.
|
inline |
Definition at line 597 of file pointer_expr.h.
|
inline |
Definition at line 515 of file pointer_expr.h.
|
inline |
Definition at line 315 of file pointer_expr.h.
|
inline |
Definition at line 431 of file pointer_expr.h.
|
inline |
Definition at line 206 of file pointer_expr.h.