Go to the documentation of this file.
48 bool seen_symbol =
false;
51 if(it->id() == ID_symbol)
65 if(pointer.
type().
id()!=ID_pointer)
66 throw "dereference expected pointer type, but got "+
70 if(pointer.
id()==ID_if)
77 else if(pointer.
id() == ID_typecast)
79 const exprt *underlying = &pointer;
82 while(underlying->
id() == ID_typecast &&
83 underlying->
type().
id() == ID_pointer)
88 if(underlying->
id() == ID_if && underlying->
type().
id() == ID_pointer)
102 std::cout <<
"value_set_dereferencet::dereference pointer=" <<
format(pointer)
107 const std::vector<exprt> points_to_set =
111 std::cout <<
"value_set_dereferencet::dereference points_to_set={";
112 for(
auto p : points_to_set)
113 std::cout <<
format(p) <<
"; ";
114 std::cout <<
"}\n" << std::flush;
118 const std::vector<exprt> retained_values =
123 exprt compare_against_pointer = pointer;
135 compare_against_pointer = fresh_binder.
symbol_expr();
139 std::cout <<
"value_set_dereferencet::dereference retained_values={";
140 for(
const auto &value : retained_values)
141 std::cout <<
format(value) <<
"; ";
142 std::cout <<
"}\n" << std::flush;
145 std::list<valuet> values =
160 for(std::list<valuet>::const_iterator
164 if(it->value.is_nil())
179 failure_value=failed_symbol->symbol_expr();
180 failure_value.
set(ID_C_invalid_object,
true);
197 failure_value.
set(ID_C_invalid_object,
true);
201 value.
value=failure_value;
203 values.push_front(value);
210 for(std::list<valuet>::const_iterator
215 if(it->value.is_not_nil())
220 value=
if_exprt(it->pointer_guard, it->value, value);
224 if(compare_against_pointer != pointer)
228 std::cout <<
"value_set_derefencet::dereference value=" <<
format(value)
245 const typet &object_type,
246 const typet &dereference_type,
249 const typet *object_unwrapped = &object_type;
250 const typet *dereference_unwrapped = &dereference_type;
251 while(object_unwrapped->
id() == ID_pointer &&
252 dereference_unwrapped->
id() == ID_pointer)
254 object_unwrapped = &object_unwrapped->
subtype();
255 dereference_unwrapped = &dereference_unwrapped->
subtype();
257 if(dereference_unwrapped->
id() == ID_empty)
261 else if(dereference_unwrapped->
id() == ID_pointer &&
262 object_unwrapped->
id() != ID_pointer)
265 std::cout <<
"value_set_dereference: the dereference type has "
266 "too many ID_pointer levels"
268 std::cout <<
" object_type: " << object_type.
pretty() << std::endl;
269 std::cout <<
" dereference_type: " << dereference_type.
pretty()
274 if(object_type == dereference_type)
280 dt_base=
ns.
follow(dereference_type);
282 if(ot_base.
id()==ID_struct &&
283 dt_base.id()==ID_struct)
291 if(dereference_type.
id()==ID_code &&
292 object_type.
id()==ID_code)
296 if((dereference_type.
id()==ID_signedbv ||
297 dereference_type.
id()==ID_unsignedbv) &&
298 (object_type.
id()==ID_signedbv ||
299 object_type.
id()==ID_unsignedbv) &&
324 bool exclude_null_derefs,
327 if(what.
id() == ID_unknown || what.
id() == ID_invalid)
335 if(root_object.
id() == ID_null_object)
339 else if(root_object.
id() == ID_integer_address)
361 const exprt &pointer_expr,
365 type_checked_cast<pointer_typet>(pointer_expr.
type());
368 if(what.
id()==ID_unknown ||
369 what.
id()==ID_invalid)
374 if(what.
id()!=ID_object_descriptor)
375 throw "unknown points-to: "+what.
id_string();
383 std::cout <<
"O: " <<
format(root_object) <<
'\n';
388 if(root_object.
id() == ID_null_object)
395 else if(root_object.
id()==ID_dynamic_object)
405 else if(root_object.
id()==ID_integer_address)
413 if(memory_symbol.
type.
subtype() == dereference_type)
423 result.
value=index_expr;
473 const typet &object_type =
object.type();
474 const typet &root_object_type = root_object.
type();
476 exprt root_object_subexpression=root_object;
490 root_object_type.
id() == ID_array &&
492 root_object_type.
subtype(), dereference_type,
ns))
506 exprt adjusted_offset;
511 if(!element_size.has_value() || *element_size == 0)
513 throw "unknown or invalid type size of:\n" +
516 else if(*element_size == 1)
519 adjusted_offset = offset;
526 offset, ID_div, element_size_expr, offset.
type());
542 root_object_subexpression, o.
offset(), dereference_type,
ns);
543 if(subexpr.has_value())
549 result.
value = subexpr.value();
583 return type.
id()==ID_unsignedbv ||
584 type.
id()==ID_signedbv ||
586 type.
id()==ID_fixedbv ||
587 type.
id()==ID_floatbv ||
588 type.
id()==ID_c_enum_tag;
601 const typet &to_type,
615 (
from_type.id() == ID_pointer && to_type.
id() == ID_pointer))
624 to_type.
id() != ID_fixedbv && to_type.
id() != ID_floatbv &&
648 const typet &to_type,
655 if(
from_type.id()==ID_code || to_type.
id()==ID_code)
674 from_type.id() == ID_array && from_type_subtype_size.has_value() &&
675 *from_type_subtype_size == 1 && to_type_size.has_value() &&
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
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 exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
virtual void get_value_set(const exprt &expr, value_setst::valuest &value_set) const =0
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
static bool memory_model(exprt &value, const typet &type, const exprt &offset, const namespacet &ns)
Replace value by an expression of type to_type corresponding to the value at memory address value + o...
depth_iteratort depth_begin()
The type of an expression, extends irept.
Fresh auxiliary symbol creation.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
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.
The trinary if-then-else operator.
Various predicates over pointers in programs.
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.
static bool should_ignore_value(const exprt &what, bool exclude_null_derefs, const irep_idt &language_mode)
Determine whether possible alias what should be ignored when replacing a pointer by its referees.
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.
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
virtual const symbolt * get_or_create_failed_symbol(const exprt &expr)=0
exprt dynamic_object(const exprt &pointer)
static bool dereference_type_compare(const typet &object_type, const typet &dereference_type, const namespacet &ns)
Check if the two types have matching number of ID_pointer levels, with the dereference type eventuall...
struct configt::ansi_ct ansi_c
Expression to hold a symbol (variable)
symbol_tablet & new_symbol_table
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
irep_idt byte_extract_id()
typet & type()
Return the type of the expression.
exprt dereference(const exprt &pointer)
Dereference the given pointer-expression.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Expression classes for byte-level operators.
The null pointer constant.
static bool should_use_local_definition_for(const exprt &expr)
Returns true if expr is complicated enough that a local definition (using a let expression) is prefer...
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)
pointer_typet pointer_type(const typet &subtype)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
Ranges: pair of begin and end iterators, which can be initialized from containers,...
static bool memory_model_bytes(exprt &value, const typet &type, const exprt &offset, const namespacet &ns)
Replace value by an expression of type to_type corresponding to the value at memory address value + o...
const exprt & root_object() const
exprt pointer_offset(const exprt &pointer)
bool is_zero() const
Return whether the expression is a constant representing 0.
Deprecated expression utility functions.
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.
Forward depth-first search iterators These iterators' copy operations are expensive,...
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
void set(const irep_namet &name, const irep_idt &value)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
optionalt< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
bool is_constant() const
Return whether the expression is a constant.
exprt same_object(const exprt &p1, const exprt &p2)
static valuet build_reference_to(const exprt &what, const exprt &pointer, const namespacet &ns)
Operator to return the address of an object.
Semantic type conversion.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
The Boolean constant true.
depth_iteratort depth_end()
const source_locationt & source_location() const
ranget< iteratort > make_range(iteratort begin, iteratort end)
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, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
irep_idt name
The unique identifier.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.