Go to the documentation of this file.
12 #ifndef CPROVER_POINTER_ANALYSIS_DEREFERENCE_H
13 #define CPROVER_POINTER_ANALYSIS_DEREFERENCE_H
62 const typet &object_type,
63 const typet &dereference_type)
const;
78 return dereference_object(pointer);
81 #endif // CPROVER_POINTER_ANALYSIS_DEREFERENCE_H
exprt dereference_typecast(const typecast_exprt &expr, const exprt &offset, const typet &type)
Attempt to dereference the object at address expr + offset and of type type.
The type of an expression, extends irept.
The trinary if-then-else operator.
exprt read_object(const exprt &object, const exprt &offset, const typet &type)
Base class for all expressions.
dereferencet(const namespacet &_ns)
exprt operator()(const exprt &pointer)
Dereference the given pointer-expression.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
exprt dereference_plus(const exprt &expr, const exprt &offset, const typet &type)
Attempt to dereference the object at address expr + offset and of type type.
Wrapper for a function which dereference a pointer-expression.
exprt dereference_rec(const exprt &address, const exprt &offset, const typet &type)
Attempt to dereference the object at address address + offset and of type type.
exprt dereference(const exprt &pointer, const namespacet &ns)
Dereference the given pointer-expression.
Semantic type conversion.
bool type_compatible(const typet &object_type, const typet &dereference_type) const
Check that it is ok to cast an object of type object_type to deference_type.
exprt dereference_if(const if_exprt &expr, const exprt &offset, const typet &type)
Attempt to dereference the object at address expr + offset and of type type.