CBMC
|
Various predicates over pointers in programs. More...
#include "std_expr.h"
Go to the source code of this file.
Classes | |
class | is_invalid_pointer_exprt |
Macros | |
#define | SYMEX_DYNAMIC_PREFIX "symex_dynamic" |
Functions | |
exprt | same_object (const exprt &p1, const exprt &p2) |
exprt | deallocated (const exprt &pointer, const namespacet &) |
exprt | dead_object (const exprt &pointer, const namespacet &) |
exprt | pointer_offset (const exprt &pointer) |
exprt | pointer_object (const exprt &pointer) |
exprt | object_size (const exprt &pointer) |
exprt | null_object (const exprt &pointer) |
exprt | integer_address (const exprt &pointer) |
exprt | object_lower_bound (const exprt &pointer, const exprt &offset) |
exprt | object_upper_bound (const exprt &pointer, const exprt &access_size) |
template<> | |
bool | can_cast_expr< is_invalid_pointer_exprt > (const exprt &base) |
void | validate_expr (const is_invalid_pointer_exprt &value) |
Various predicates over pointers in programs.
Definition in file pointer_predicates.h.
#define SYMEX_DYNAMIC_PREFIX "symex_dynamic" |
Definition at line 17 of file pointer_predicates.h.
|
inline |
Definition at line 45 of file pointer_predicates.h.
exprt dead_object | ( | const exprt & | pointer, |
const namespacet & | ns | ||
) |
Definition at line 51 of file pointer_predicates.cpp.
exprt deallocated | ( | const exprt & | pointer, |
const namespacet & | ns | ||
) |
Definition at line 43 of file pointer_predicates.cpp.
Definition at line 65 of file pointer_predicates.cpp.
Definition at line 59 of file pointer_predicates.cpp.
Definition at line 117 of file pointer_predicates.cpp.
Definition at line 33 of file pointer_predicates.cpp.
Definition at line 72 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 50 of file pointer_predicates.h.