CBMC
|
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 | pointer_in_range_exprt |
pointer_in_range(a, b, c) evaluates to true iff same_object(a, b, c) ∧ r_ok(a, offset(c)-offset(a)) ∧ a<=b ∧ b<=c Note that the last inequality is weak, i.e., b may be equal to c. 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... | |
class | annotated_pointer_constant_exprt |
Pointer-typed bitvector constant annotated with the pointer expression that the bitvector is the numeric representation of. More... | |
class | pointer_offset_exprt |
The offset (in bytes) of a pointer relative to the object. More... | |
class | pointer_object_exprt |
A numerical identifier for the object a pointer points to. More... | |
class | object_size_exprt |
Expression for finding the size (in bytes) of the object a pointer points to. More... | |
class | is_cstring_exprt |
A predicate that indicates that a zero-terminated string starts at the given address. More... | |
class | cstrlen_exprt |
An expression, akin to ISO C's strlen, that denotes the length of a zero-terminated string that starts at the given address. More... | |
class | live_object_exprt |
A predicate that indicates that the object pointed to is live. More... | |
class | writeable_object_exprt |
A predicate that indicates that the object pointed to is writeable. More... | |
class | separate_exprt |
A predicate that indicates that the objects pointed to are distinct. More... | |
API to expression classes for Pointers.
Definition in file pointer_expr.h.
|
inline |
Definition at line 459 of file pointer_expr.h.
|
inline |
Definition at line 955 of file pointer_expr.h.
|
inline |
Definition at line 1249 of file pointer_expr.h.
|
inline |
Definition at line 772 of file pointer_expr.h.
|
inline |
Definition at line 285 of file pointer_expr.h.
|
inline |
Definition at line 696 of file pointer_expr.h.
|
inline |
Definition at line 609 of file pointer_expr.h.
|
inline |
Definition at line 1191 of file pointer_expr.h.
|
inline |
Definition at line 340 of file pointer_expr.h.
|
inline |
Definition at line 1305 of file pointer_expr.h.
|
inline |
Definition at line 525 of file pointer_expr.h.
|
inline |
Definition at line 221 of file pointer_expr.h.
|
inline |
Definition at line 1154 of file pointer_expr.h.
|
inline |
Definition at line 408 of file pointer_expr.h.
|
inline |
Definition at line 1072 of file pointer_expr.h.
|
inline |
Definition at line 1014 of file pointer_expr.h.
|
inline |
Definition at line 867 of file pointer_expr.h.
|
inline |
Definition at line 837 of file pointer_expr.h.
|
inline |
Definition at line 1415 of file pointer_expr.h.
|
inline |
Definition at line 896 of file pointer_expr.h.
|
inline |
Definition at line 1361 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 66 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 135 of file pointer_expr.h.
bool is_reference | ( | const typet & | type | ) |
Returns true if the type is a reference.
Definition at line 143 of file std_types.cpp.
bool is_rvalue_reference | ( | const typet & | type | ) |
Returns if the type is an R value reference.
Definition at line 150 of file std_types.cpp.
|
inline |
This method tests, if the given typet is a pointer of type void.
Definition at line 96 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 475 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 484 of file pointer_expr.h.
|
inline |
Cast an exprt to an annotated_pointer_constant_exprt.
expr must be known to be annotated_pointer_constant_exprt.
expr | Source expression |
Definition at line 973 of file pointer_expr.h.
|
inline |
Cast an exprt to an annotated_pointer_constant_exprt.
expr must be known to be annotated_pointer_constant_exprt.
expr | Source expression |
Definition at line 984 of file pointer_expr.h.
|
inline |
Cast an exprt to a cstrlen_exprt.
expr must be known to be cstrlen_exprt.
expr | Source expression |
Definition at line 1265 of file pointer_expr.h.
|
inline |
Cast an exprt to a cstrlen_exprt.
expr must be known to be cstrlen_exprt.
expr | Source expression |
Definition at line 1274 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 788 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 797 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 301 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 311 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 712 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 722 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 625 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 635 of file pointer_expr.h.
|
inline |
Cast an exprt to a is_cstring_exprt.
expr must be known to be is_cstring_exprt.
expr | Source expression |
Definition at line 1207 of file pointer_expr.h.
|
inline |
Cast an exprt to a is_cstring_exprt.
expr must be known to be is_cstring_exprt.
expr | Source expression |
Definition at line 1216 of file pointer_expr.h.
|
inline |
Definition at line 351 of file pointer_expr.h.
|
inline |
Definition at line 361 of file pointer_expr.h.
|
inline |
Cast an exprt to a live_object_exprt.
expr must be known to be live_object_exprt.
expr | Source expression |
Definition at line 1321 of file pointer_expr.h.
|
inline |
Cast an exprt to a live_object_exprt.
expr must be known to be live_object_exprt.
expr | Source expression |
Definition at line 1330 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 541 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 551 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 238 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 248 of file pointer_expr.h.
|
inline |
Cast an exprt to a object_size_exprt.
expr must be known to be object_size_exprt.
expr | Source expression |
Definition at line 1136 of file pointer_expr.h.
|
inline |
Cast an exprt to a object_size_exprt.
expr must be known to be object_size_exprt.
expr | Source expression |
Definition at line 1145 of file pointer_expr.h.
|
inline |
Definition at line 418 of file pointer_expr.h.
|
inline |
Definition at line 428 of file pointer_expr.h.
|
inline |
Cast an exprt to a pointer_object_exprt.
expr must be known to be pointer_object_exprt.
expr | Source expression |
Definition at line 1091 of file pointer_expr.h.
|
inline |
Cast an exprt to a pointer_object_exprt.
expr must be known to be pointer_object_exprt.
expr | Source expression |
Definition at line 1101 of file pointer_expr.h.
|
inline |
Cast an exprt to a pointer_offset_exprt.
expr must be known to be pointer_offset_exprt.
expr | Source expression |
Definition at line 1033 of file pointer_expr.h.
|
inline |
Cast an exprt to a pointer_offset_exprt.
expr must be known to be pointer_offset_exprt.
expr | Source expression |
Definition at line 1043 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 79 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 87 of file pointer_expr.h.
|
inline |
Definition at line 877 of file pointer_expr.h.
|
inline |
Definition at line 847 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 148 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 155 of file pointer_expr.h.
|
inline |
Cast an exprt to a separate_exprt.
expr must be known to be separate_exprt.
expr | Source expression |
Definition at line 1430 of file pointer_expr.h.
|
inline |
Cast an exprt to a separate_exprt.
expr must be known to be separate_exprt.
expr | Source expression |
Definition at line 1439 of file pointer_expr.h.
|
inline |
Definition at line 906 of file pointer_expr.h.
|
inline |
Cast an exprt to a writeable_object_exprt.
expr must be known to be writeable_object_exprt.
expr | Source expression |
Definition at line 1377 of file pointer_expr.h.
|
inline |
Cast an exprt to a writeable_object_exprt.
expr must be known to be writeable_object_exprt.
expr | Source expression |
Definition at line 1387 of file pointer_expr.h.
|
inline |
Definition at line 464 of file pointer_expr.h.
|
inline |
Definition at line 960 of file pointer_expr.h.
|
inline |
Definition at line 1254 of file pointer_expr.h.
|
inline |
Definition at line 777 of file pointer_expr.h.
|
inline |
Definition at line 290 of file pointer_expr.h.
|
inline |
Definition at line 701 of file pointer_expr.h.
|
inline |
Definition at line 614 of file pointer_expr.h.
|
inline |
Definition at line 1196 of file pointer_expr.h.
|
inline |
Definition at line 345 of file pointer_expr.h.
|
inline |
Definition at line 1310 of file pointer_expr.h.
|
inline |
Definition at line 530 of file pointer_expr.h.
|
inline |
Definition at line 226 of file pointer_expr.h.
|
inline |
Definition at line 1159 of file pointer_expr.h.
|
inline |
Definition at line 413 of file pointer_expr.h.
|
inline |
Definition at line 1077 of file pointer_expr.h.
|
inline |
Definition at line 1019 of file pointer_expr.h.
|
inline |
Definition at line 872 of file pointer_expr.h.
|
inline |
Definition at line 842 of file pointer_expr.h.
|
inline |
Definition at line 1420 of file pointer_expr.h.
|
inline |
Definition at line 901 of file pointer_expr.h.
|
inline |
Definition at line 1366 of file pointer_expr.h.