12 #ifndef CPROVER_POINTER_ANALYSIS_DEREFERENCE_H 13 #define CPROVER_POINTER_ANALYSIS_DEREFERENCE_H 75 const typet &object_type,
76 const typet &dereference_type)
const;
80 const exprt &offset)
const;
91 return dereference_object(pointer);
94 #endif // CPROVER_POINTER_ANALYSIS_DEREFERENCE_H The type of an expression.
exprt dereference_rec(const exprt &address, const exprt &offset, const typet &type)
exprt dereference_if(const if_exprt &expr, const exprt &offset, const typet &type)
The trinary if-then-else operator.
exprt dereference_typecast(const typecast_exprt &expr, const exprt &offset, const typet &type)
bool type_compatible(const typet &object_type, const typet &dereference_type) const
exprt dereference(const exprt &pointer, const namespacet &ns)
Base class for all expressions.
exprt dereference_plus(const exprt &expr, const exprt &offset, const typet &type)
dereferencet(const namespacet &_ns)
Constructor.
exprt operator()(const exprt &pointer)
void offset_sum(exprt &dest, const exprt &offset) const
exprt read_object(const exprt &object, const exprt &offset, const typet &type)