Go to the documentation of this file.
40 if(pointer.
type().
id()!=ID_pointer)
41 throw "dereference expected pointer type, but got "+
45 if(pointer.
id()==ID_if)
65 std::cout <<
"DEREF: " <<
format(pointer) <<
'\n';
74 for(value_setst::valuest::const_iterator
75 it=points_to_set.begin();
76 it!=points_to_set.end();
78 std::cout <<
"P: " <<
format(*it) <<
'\n';
83 std::list<valuet> values;
85 for(value_setst::valuest::const_iterator
86 it=points_to_set.begin();
87 it!=points_to_set.end();
96 std::cout <<
" (ignored)";
101 values.push_back(value);
114 for(std::list<valuet>::const_iterator
118 if(it->value.is_nil())
130 pointer, failed_symbol))
134 failure_value.
set(ID_C_invalid_object,
true);
151 failure_value.
set(ID_C_invalid_object,
true);
155 value.
value=failure_value;
157 values.push_front(value);
164 for(std::list<valuet>::const_iterator
169 if(it->value.is_not_nil())
174 value=
if_exprt(it->pointer_guard, it->value, value);
179 std::cout <<
"R: " <<
format(value) <<
"\n\n";
194 const typet &object_type,
195 const typet &dereference_type)
const
197 const typet *object_unwrapped = &object_type;
198 const typet *dereference_unwrapped = &dereference_type;
199 while(object_unwrapped->
id() == ID_pointer &&
200 dereference_unwrapped->
id() == ID_pointer)
202 object_unwrapped = &object_unwrapped->
subtype();
203 dereference_unwrapped = &dereference_unwrapped->
subtype();
205 if(dereference_unwrapped->
id() == ID_empty)
209 else if(dereference_unwrapped->
id() == ID_pointer &&
210 object_unwrapped->
id() != ID_pointer)
213 std::cout <<
"value_set_dereference: the dereference type has "
214 "too many ID_pointer levels"
216 std::cout <<
" object_type: " << object_type.
pretty() << std::endl;
217 std::cout <<
" dereference_type: " << dereference_type.
pretty()
228 dt_base=
ns.
follow(dereference_type);
230 if(ot_base.
id()==ID_struct &&
231 dt_base.id()==ID_struct)
239 if(dereference_type.
id()==ID_code &&
240 object_type.
id()==ID_code)
244 if((dereference_type.
id()==ID_signedbv ||
245 dereference_type.
id()==ID_unsignedbv) &&
246 (object_type.
id()==ID_signedbv ||
247 object_type.
id()==ID_unsignedbv) &&
273 const exprt &pointer_expr)
275 const typet &dereference_type=
278 if(what.
id()==ID_unknown ||
279 what.
id()==ID_invalid)
284 if(what.
id()!=ID_object_descriptor)
285 throw "unknown points-to: "+what.
id_string();
293 std::cout <<
"O: " <<
format(root_object) <<
'\n';
298 if(root_object.
id() == ID_null_object)
305 else if(root_object.
id()==ID_dynamic_object)
323 else if(root_object.
id()==ID_integer_address)
339 dereference_type,
ns))
349 result.
value=index_expr;
386 equal_exprt equality(pointer_expr, object_pointer);
401 exprt root_object_subexpression=root_object;
411 if(object_type!=
ns.
follow(dereference_type))
414 else if(root_object_type.
id()==ID_array &&
431 exprt adjusted_offset;
436 if(!element_size.has_value() || *element_size == 0)
438 throw "unknown or invalid type size of:\n" +
441 else if(*element_size == 1)
444 adjusted_offset = offset;
451 offset, ID_div, element_size_expr, offset.
type());
459 result.
value=index_expr;
468 root_object_subexpression, o.
offset(), dereference_type,
ns);
475 result.
value = subexpr;
505 return type.
id()==ID_unsignedbv ||
506 type.
id()==ID_signedbv ||
508 type.
id()==ID_fixedbv ||
509 type.
id()==ID_floatbv ||
510 type.
id()==ID_c_enum_tag;
523 const typet &to_type,
536 (
from_type.id() == ID_pointer && to_type.
id() == ID_pointer))
545 to_type.
id() != ID_fixedbv && to_type.
id() != ID_floatbv &&
569 const typet &to_type,
575 if(
from_type.id()==ID_code || to_type.
id()==ID_code)
589 auto from_type_subtype_size =
596 from_type_subtype_size.has_value() && *from_type_subtype_size == 1 &&
597 to_type_size.has_value() && *to_type_size == 1 &&
static exprt conditional_cast(const exprt &expr, const typet &type)
const typet & subtype() const
Return value for build_reference_to; see that method for documentation.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
The type of an expression, extends irept.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
typet type
Type of symbol.
Operator to dereference a pointer.
void add(const exprt &expr)
The trinary if-then-else operator.
const irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use,...
Split an expression into a base object and a (byte) offset.
virtual void get_value_set(const exprt &expr, value_setst::valuest &value_set)=0
const bool exclude_null_derefs
Flag indicating whether value_set_dereferencet::dereference should disregard an apparent attempt to d...
Base class for all expressions.
A base class for binary expressions.
virtual exprt dereference(const exprt &pointer, const guardt &guard, const modet mode)
Dereference the given pointer-expression.
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
exprt dynamic_object(const exprt &pointer)
struct configt::ansi_ct ansi_c
Expression to hold a symbol (variable)
symbol_tablet & new_symbol_table
irep_idt byte_extract_id()
typet & type()
Return the type of the expression.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Expression classes for byte-level operators.
std::list< exprt > valuest
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
dereference_callbackt & dereference_callback
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
const std::string & id_string() const
bool simplify(exprt &expr, const namespacet &ns)
const irep_idt & id() const
const exprt & root_object() const
exprt pointer_offset(const exprt &pointer)
bool memory_model_bytes(exprt &value, const typet &type, const exprt &offset)
Replace value by an expression of type to_type corresponding to the value at memory address value + o...
exprt malloc_object(const exprt &pointer, const namespacet &ns)
bool is_zero() const
Return whether the expression is a constant representing 0.
static bool is_a_bv_type(const typet &type)
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
virtual bool has_failed_symbol(const exprt &expr, const symbolt *&symbol)=0
bool dereference_type_compare(const typet &object_type, const typet &dereference_type) const
Check if the two types have matching number of ID_pointer levels, with the dereference type eventuall...
void set(const irep_namet &name, const irep_idt &value)
bool is_constant() const
Return whether the expression is a constant.
exprt same_object(const exprt &p1, const exprt &p2)
bool memory_model(exprt &value, const typet &type, const exprt &offset)
Replace value by an expression of type to_type corresponding to the value at memory address value + o...
Operator to return the address of an object.
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
Semantic type conversion.
The Boolean constant true.
const source_locationt & source_location() const
exprt get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
irep_idt name
The unique identifier.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
valuet build_reference_to(const exprt &what, const exprt &pointer)