cprover
|
Wrapper for a function which dereference a pointer-expression. More...
#include <dereference.h>
Public Member Functions | |
dereferencet (const namespacet &_ns) | |
~dereferencet () | |
exprt | operator() (const exprt &pointer) |
Dereference the given pointer-expression. More... | |
Private Member Functions | |
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 . More... | |
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 . More... | |
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 . More... | |
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 . More... | |
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 . More... | |
exprt | read_object (const exprt &object, const exprt &offset, const typet &type) |
Private Attributes | |
const namespacet & | ns |
Wrapper for a function which dereference a pointer-expression.
Definition at line 22 of file dereference.h.
|
inlineexplicit |
Definition at line 25 of file dereference.h.
|
inline |
Definition at line 31 of file dereference.h.
|
private |
Attempt to dereference the object at address expr + offset
and of type type
.
Throws an exception if unsuccessful.
This is done by dereferencing both the true and false cases of the if expression and putting the result together in a new if expression with the same condition.
Definition at line 218 of file dereference.cpp.
|
private |
Attempt to dereference the object at address expr + offset
and of type type
.
Throws an exception if unsuccessful. This assumes expr
is a plus_exprt
but does not check for it.
Definition at line 233 of file dereference.cpp.
|
private |
Attempt to dereference the object at address address + offset
and of type type
.
Throws an exception if unsuccessful.
Definition at line 157 of file dereference.cpp.
|
private |
Attempt to dereference the object at address expr + offset
and of type type
.
Throws an exception if unsuccessful.
If expr
is a typecast of the form (type)ptr
:
ptr
is of pointer type, dereference ptr + offset
ptr
is of integer type, return an integer_dereference expressionDefinition at line 276 of file dereference.cpp.
Dereference the given pointer-expression.
pointer | A pointer-typed expression, to be dereferenced. |
Definition at line 28 of file dereference.cpp.
|
private |
byte_extract(object, offset)
and of type type
. The expression is potentially simplified so that for instance in the case of an array, object[offset]
can be returned. Definition at line 50 of file dereference.cpp.
|
private |
Check that it is ok to cast an object of type object_type
to deference_type
.
Definition at line 307 of file dereference.cpp.
|
private |
Definition at line 39 of file dereference.h.