cprover
|
Various predicates over pointers in programs. More...
Go to the source code of this file.
Classes | |
class | is_invalid_pointer_exprt |
Macros | |
#define | SYMEX_DYNAMIC_PREFIX "symex_dynamic::" |
Various predicates over pointers in programs.
Definition in file pointer_predicates.h.
#define SYMEX_DYNAMIC_PREFIX "symex_dynamic::" |
Definition at line 18 of file pointer_predicates.h.
|
inline |
Definition at line 63 of file pointer_predicates.h.
exprt dead_object | ( | const exprt & | pointer, |
const namespacet & | ns | ||
) |
Definition at line 59 of file pointer_predicates.cpp.
exprt deallocated | ( | const exprt & | pointer, |
const namespacet & | ns | ||
) |
Definition at line 51 of file pointer_predicates.cpp.
Definition at line 72 of file pointer_predicates.cpp.
Definition at line 126 of file pointer_predicates.cpp.
exprt dynamic_object_upper_bound | ( | const exprt & | pointer, |
const namespacet & | ns, | ||
const exprt & | access_size | ||
) |
Definition at line 133 of file pointer_predicates.cpp.
exprt dynamic_size | ( | const namespacet & | ns | ) |
Definition at line 67 of file pointer_predicates.cpp.
Definition at line 79 of file pointer_predicates.cpp.
exprt good_pointer_def | ( | const exprt & | pointer, |
const namespacet & | ns | ||
) |
Definition at line 84 of file pointer_predicates.cpp.
Definition at line 113 of file pointer_predicates.cpp.
exprt malloc_object | ( | const exprt & | pointer, |
const namespacet & | ns | ||
) |
Definition at line 43 of file pointer_predicates.cpp.
Definition at line 107 of file pointer_predicates.cpp.
Definition at line 120 of file pointer_predicates.cpp.
Definition at line 192 of file pointer_predicates.cpp.
Definition at line 33 of file pointer_predicates.cpp.
Definition at line 162 of file pointer_predicates.cpp.
Definition at line 23 of file pointer_predicates.cpp.
Definition at line 38 of file pointer_predicates.cpp.
Definition at line 28 of file pointer_predicates.cpp.
|
inline |
Definition at line 68 of file pointer_predicates.h.