cprover
|
Go to the source code of this file.
Various predicates over pointers in programs
Definition in file pointer_predicates.h.
exprt dead_object | ( | const exprt & | pointer, |
const namespacet & | |||
) |
Definition at line 58 of file pointer_predicates.cpp.
exprt deallocated | ( | const exprt & | pointer, |
const namespacet & | |||
) |
Definition at line 50 of file pointer_predicates.cpp.
Definition at line 71 of file pointer_predicates.cpp.
exprt dynamic_object_lower_bound | ( | const exprt & | pointer, |
const namespacet & | , | ||
const exprt & | offset | ||
) |
Definition at line 146 of file pointer_predicates.cpp.
exprt dynamic_object_upper_bound | ( | const exprt & | pointer, |
const namespacet & | , | ||
const exprt & | access_size | ||
) |
Definition at line 154 of file pointer_predicates.cpp.
exprt dynamic_size | ( | const namespacet & | ) |
Definition at line 66 of file pointer_predicates.cpp.
Definition at line 78 of file pointer_predicates.cpp.
exprt good_pointer_def | ( | const exprt & | pointer, |
const namespacet & | |||
) |
Definition at line 83 of file pointer_predicates.cpp.
Definition at line 128 of file pointer_predicates.cpp.
Definition at line 141 of file pointer_predicates.cpp.
exprt malloc_object | ( | const exprt & | pointer, |
const namespacet & | |||
) |
Definition at line 42 of file pointer_predicates.cpp.
Definition at line 122 of file pointer_predicates.cpp.
Definition at line 135 of file pointer_predicates.cpp.
exprt object_lower_bound | ( | const exprt & | pointer, |
const namespacet & | , | ||
const exprt & | offset | ||
) |
Definition at line 221 of file pointer_predicates.cpp.
Definition at line 32 of file pointer_predicates.cpp.
exprt object_upper_bound | ( | const exprt & | pointer, |
const namespacet & | , | ||
const exprt & | access_size | ||
) |
Definition at line 187 of file pointer_predicates.cpp.
Definition at line 22 of file pointer_predicates.cpp.
Definition at line 37 of file pointer_predicates.cpp.
Definition at line 27 of file pointer_predicates.cpp.