57 if(expr.
id()==ID_member || expr.
id()==ID_index)
71 if(pointer.
type().
id()!=ID_pointer)
72 throw "dereference expected pointer type, but got "+
76 if(pointer.
id()==ID_if)
96 std::cout <<
"DEREF: " <<
from_expr(
ns,
"", pointer) <<
'\n';
105 for(value_setst::valuest::const_iterator
106 it=points_to_set.begin();
107 it!=points_to_set.end();
109 std::cout <<
"P: " <<
from_expr(
ns,
"", *it) <<
'\n';
114 std::list<valuet> values;
116 for(value_setst::valuest::const_iterator
117 it=points_to_set.begin();
118 it!=points_to_set.end();
128 values.push_back(value);
142 for(std::list<valuet>::const_iterator
146 if(it->value.is_nil())
158 pointer, failed_symbol))
162 failure_value.
set(ID_C_invalid_object,
true);
179 failure_value.
set(ID_C_invalid_object,
true);
185 value.
value=failure_value;
187 values.push_front(value);
194 for(std::list<valuet>::const_iterator
199 if(it->value.is_not_nil())
204 value=
if_exprt(it->pointer_guard, it->value, value);
209 std::cout <<
"R: " <<
from_expr(
ns,
"", value) <<
"\n\n";
216 const typet &object_type,
217 const typet &dereference_type)
const 219 if(dereference_type.
id()==ID_empty)
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) &&
258 const exprt &pointer,
269 "pointer dereference",
277 const exprt &pointer_expr,
280 const typet &dereference_type=
283 if(what.
id()==ID_unknown ||
284 what.
id()==ID_invalid)
290 if(what.
id()!=ID_object_descriptor)
291 throw "unknown points-to: "+what.
id_string();
299 std::cout <<
"O: " <<
from_expr(
ns,
"", root_object) <<
'\n';
304 if(root_object.
id()==
"NULL-object")
315 "pointer dereference",
316 "NULL pointer", tmp_guard);
323 "pointer dereference",
324 "NULL plus offset pointer", tmp_guard);
328 else if(root_object.
id()==ID_dynamic_object)
357 "pointer dereference",
358 "dynamic object deallocated",
368 tmp_guard.
add(is_malloc_object);
375 "pointer dereference",
376 "dynamic object lower bound", tmp_guard);
386 tmp_guard.
add(is_malloc_object);
394 "pointer dereference",
395 "dynamic object upper bound", tmp_guard);
400 else if(root_object.
id()==ID_integer_address)
416 dereference_type,
ns))
423 result.
value=index_expr;
446 result.
value=byte_extract;
457 equal_exprt equality(pointer_expr, object_pointer);
478 exprt root_object_subexpression=root_object;
488 if(object_type!=
ns.
follow(dereference_type))
491 else if(root_object_type.
id()==ID_array &&
508 exprt adjusted_offset;
512 dereference_type.
id()==ID_empty?
519 adjusted_offset=offset;
521 else if(element_size<=0)
523 throw "unknown or invalid type size of:\n"+dereference_type.
pretty();
527 exprt element_size_expr=
531 offset, ID_div, element_size_expr, offset.
type());
541 result.
value=index_expr;
547 root_object_subexpression,
554 result.
value=root_object_subexpression;
572 std::string msg=
"memory model not applicable (got `";
574 msg+=
"', expected `";
579 "pointer dereference",
601 if(symbol_expr.
id()==ID_string_constant)
608 "pointer dereference",
609 "write access to string constant",
613 else if(symbol_expr.
is_nil() ||
614 symbol_expr.
get_bool(ID_C_invalid_object))
619 else if(symbol_expr.
id()==ID_symbol)
631 "pointer dereference",
655 if(array_type.
id()!=ID_array)
656 throw "bounds check expected array type";
671 throw "no zero constant of index type "+
675 inequality(expr.
index(), ID_lt, zero);
678 tmp_guard.add(inequality);
681 name+
" lower bound", tmp_guard);
685 const exprt &size_expr=
688 if(size_expr.
id()==ID_infinity)
698 throw "index array operand of wrong type";
704 inequality.op1().type(),
706 throw "index address of wrong type";
709 tmp_guard.
add(inequality);
712 name+
" upper bound", tmp_guard);
720 if(type.
id()==ID_c_enum_tag)
723 assert(t.
id()==ID_c_enum);
732 return type.
id()==ID_unsignedbv ||
733 type.
id()==ID_signedbv ||
735 type.
id()==ID_fixedbv ||
736 type.
id()==ID_floatbv ||
737 type.
id()==ID_c_enum_tag;
742 const typet &to_type,
762 if(to_type.
id()==ID_fixedbv || to_type.
id()==ID_floatbv ||
763 from_type.
id()==ID_fixedbv || from_type.
id()==ID_floatbv)
773 if(from_type.
id()==ID_pointer &&
774 to_type.
id()==ID_pointer)
787 const typet &to_type,
803 tmp_guard.
add(offset_not_zero);
806 "offset not zero", tmp_guard);
814 const typet &to_type,
821 if(from_type.
id()==ID_code || to_type.
id()==ID_code)
865 "unknown or invalid type size:\n"+from_type.
pretty());
868 to_type.
id()==ID_empty?
871 to_width.is_not_nil(),
872 "unknown or invalid type size:\n"+to_type.
pretty());
874 from_width.
type()==to_width.type(),
875 "type mismatch on result of size_of_expr");
878 if(bound.type()!=offset.
type())
879 bound.make_typecast(offset.
type());
882 offset_upper_bound(offset, ID_gt, bound);
885 tmp_guard.
add(offset_upper_bound);
887 "pointer dereference",
888 "object upper bound", tmp_guard);
899 tmp_guard.
add(offset_lower_bound);
901 "pointer dereference",
902 "object lower bound", tmp_guard);
The type of an expression.
irep_idt name
The unique identifier.
exprt size_of_expr(const typet &type, const namespacet &ns)
const typet & follow(const typet &src) const
struct configt::ansi_ct ansi_c
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
A generic base class for relations, i.e., binary predicates.
static const exprt & get_symbol(const exprt &object)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
virtual exprt dereference(const exprt &pointer, const guardt &guard, const modet mode)
virtual void dereference_failure(const std::string &property, const std::string &msg, const guardt &guard)=0
Deprecated expression utility functions.
dereference_callbackt & dereference_callback
unsigned unsafe_string2unsigned(const std::string &str, int base)
void copy_to_operands(const exprt &expr)
const irep_idt & get_identifier() const
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
void invalid_pointer(const exprt &expr, const guardt &guard)
const exprt & root_object() const
The trinary if-then-else operator.
unsignedbv_typet size_type()
bool memory_model(exprt &value, const typet &type, const guardt &guard, const exprt &offset)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
bool get_bool(const irep_namet &name) const
virtual bool has_failed_symbol(const exprt &expr, const symbolt *&symbol)=0
exprt deallocated(const exprt &pointer, const namespacet &ns)
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
exprt null_object(const exprt &pointer)
void valid_check(const exprt &expr, const guardt &guard, const modet mode)
#define INVARIANT(CONDITION, REASON)
static unsigned invalid_counter
const typet & follow_tag(const union_tag_typet &src) const
const irep_idt & id() const
void bounds_check(const index_exprt &expr, const guardt &guard)
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Expression classes for byte-level operators.
The boolean constant true.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a generic typet to a c_enum_tag_typet.
bool memory_model_bytes(exprt &value, const typet &type, const guardt &guard, const exprt &offset)
A generic base class for binary expressions.
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
bool get_subexpression_at_offset(exprt &result, mp_integer offset, const typet &target_type_raw, const namespacet &ns)
Operator to dereference a pointer.
API to expression classes.
bool get_bool_option(const std::string &option) const
irep_idt byte_extract_id()
split an expression into a base object and a (byte) offset
const exprt & size() const
static bool is_a_bv_type(const typet &type)
valuet build_reference_to(const exprt &what, const modet mode, const exprt &pointer, const guardt &guard)
Operator to return the address of an object.
Various predicates over pointers in programs.
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
exprt dynamic_object_lower_bound(const exprt &pointer, const namespacet &ns, const exprt &offset)
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
bool has_subexpr(const exprt &src, const irep_idt &id)
returns true if the expression has a subexpression with given ID
std::size_t get_width() const
bool c_implicit_typecast(exprt &expr, const typet &dest_type, const namespacet &ns)
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast a generic exprt to an object_descriptor_exprt.
virtual void get_value_set(const exprt &expr, value_setst::valuest &value_set)=0
exprt malloc_object(const exprt &pointer, const namespacet &ns)
static unsigned bv_width(const typet &type, const namespacet &ns)
typet type
Type of symbol.
bool is_prefix_of(const struct_typet &other) const
exprt dynamic_object_upper_bound(const exprt &pointer, const typet &dereference_type, const namespacet &ns, const exprt &access_size)
Base class for all expressions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
irep_idt base_name
Base (non-scoped) name.
exprt pointer_offset(const exprt &pointer)
static bool has_dereference(const exprt &expr)
Returns 'true' iff the given expression contains unary '*'.
irep_idt get_object_name() const
bool is_ssa_expr(const exprt &expr)
symbol_tablet & new_symbol_table
const std::string & get_string(const irep_namet &name) const
const std::string & id_string() const
Expression to hold a symbol (variable)
exprt null_pointer(const exprt &pointer)
const typet & subtype() const
const irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use...
std::list< exprt > valuest
exprt same_object(const exprt &p1, const exprt &p2)
void get_new_name(symbolt &symbol, const namespacet &ns)
automated variable renaming
bool memory_model_conversion(exprt &value, const typet &type, const guardt &guard, const exprt &offset)
void make_typecast(const typet &_type)
bitvector_typet char_type()
void add(const exprt &expr)
void set(const irep_namet &name, const irep_idt &value)
bool dereference_type_compare(const typet &object_type, const typet &dereference_type) const
std::string array_name(const namespacet &ns, const exprt &expr)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.