cprover
|
TO_BE_DOCUMENTED. More...
#include <dereference.h>
Public Member Functions | |
dereferencet (const namespacet &_ns) | |
Constructor. More... | |
~dereferencet () | |
exprt | operator() (const exprt &pointer) |
Private Member Functions | |
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) |
exprt | dereference_plus (const exprt &expr, const exprt &offset, const typet &type) |
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 |
void | offset_sum (exprt &dest, const exprt &offset) const |
exprt | read_object (const exprt &object, const exprt &offset, const typet &type) |
Private Attributes | |
const namespacet & | ns |
TO_BE_DOCUMENTED.
Definition at line 23 of file dereference.h.
|
inlineexplicit |
Constructor.
_ns | Namespace |
_new_symbol_table | A symbol_table to store new symbols in |
_options | Options, in particular whether pointer checks are to be performed |
_dereference_callback | Callback object for error reporting |
Definition at line 33 of file dereference.h.
|
inline |
Definition at line 39 of file dereference.h.
References operator()().
|
private |
Definition at line 207 of file dereference.cpp.
References if_exprt::cond(), dereference_rec(), if_exprt::false_case(), if_exprt::true_case(), and exprt::type().
Referenced by dereference_rec().
|
private |
Definition at line 219 of file dereference.cpp.
References dereference_rec(), namespace_baset::follow(), irept::id(), irept::is_nil(), exprt::make_typecast(), ns, exprt::op0(), exprt::op1(), exprt::operands(), size_of_expr(), typet::subtype(), and exprt::type().
Referenced by dereference_rec().
|
private |
Definition at line 153 of file dereference.cpp.
References dereference_if(), dereference_plus(), dereference_typecast(), namespace_baset::follow(), from_integer(), constant_exprt::get_value(), irept::id(), irept::id_string(), index_type(), ns, address_of_exprt::object(), exprt::operands(), irept::pretty(), read_object(), to_address_of_expr(), to_constant_expr(), to_if_expr(), to_typecast_expr(), and exprt::type().
Referenced by dereference_if(), dereference_plus(), dereference_typecast(), and operator()().
|
private |
Definition at line 254 of file dereference.cpp.
References dereference_rec(), namespace_baset::follow(), irept::id(), exprt::is_zero(), ns, typecast_exprt::op(), pointer_type(), and exprt::type().
Referenced by dereference_rec().
The operator '()' dereferences the given pointer-expression.
pointer | A pointer-typed expression, to be dereferenced. |
Definition at line 30 of file dereference.cpp.
References dereference_rec(), from_expr(), from_integer(), irept::id(), index_type(), ns, irept::pretty(), typet::subtype(), and exprt::type().
Referenced by ~dereferencet().
|
private |
Definition at line 49 of file dereference.cpp.
References index_exprt::array(), base_type_eq(), byte_extract_id(), namespace_baset::follow(), from_integer(), member_exprt::get_component_name(), irept::id(), index_exprt::index(), irept::is_nil(), irept::is_not_nil(), exprt::is_zero(), exprt::make_typecast(), member_offset(), member_offset_expr(), ns, simplify_expr(), size_of_expr(), member_exprt::struct_op(), typet::subtype(), to_index_expr(), to_integer(), to_member_expr(), to_struct_type(), exprt::type(), and type_compatible().
Referenced by dereference_rec().
|
private |
Definition at line 286 of file dereference.cpp.
References base_type_eq(), irept::get(), irept::id(), struct_typet::is_prefix_of(), ns, and to_struct_type().
Referenced by read_object().
|
private |
Definition at line 52 of file dereference.h.
Referenced by dereference_plus(), dereference_rec(), dereference_typecast(), operator()(), read_object(), and type_compatible().