39 if(expr.
id()==ID_member || expr.
id()==ID_index)
53 if(pointer.
type().
id()!=ID_pointer)
54 throw "dereference expected pointer type, but got "+
58 if(pointer.
id()==ID_if)
78 std::cout <<
"DEREF: " <<
format(pointer) <<
'\n';
87 for(value_setst::valuest::const_iterator
88 it=points_to_set.begin();
89 it!=points_to_set.end();
91 std::cout <<
"P: " <<
format(*it) <<
'\n';
96 std::list<valuet> values;
98 for(value_setst::valuest::const_iterator
99 it=points_to_set.begin();
100 it!=points_to_set.end();
109 std::cout <<
" (ignored)";
114 values.push_back(value);
128 for(std::list<valuet>::const_iterator
132 if(it->value.is_nil())
144 pointer, failed_symbol))
148 failure_value.
set(ID_C_invalid_object,
true);
165 failure_value.
set(ID_C_invalid_object,
true);
169 value.
value=failure_value;
171 values.push_front(value);
178 for(std::list<valuet>::const_iterator
183 if(it->value.is_not_nil())
188 value=
if_exprt(it->pointer_guard, it->value, value);
193 std::cout <<
"R: " <<
format(value) <<
"\n\n";
200 const typet &object_type,
201 const typet &dereference_type)
const 211 const typet *object_unwrapped = &object_type;
212 const typet *dereference_unwrapped = &dereference_type;
213 while(object_unwrapped->
id() == ID_pointer &&
214 dereference_unwrapped->
id() == ID_pointer)
216 object_unwrapped = &object_unwrapped->
subtype();
217 dereference_unwrapped = &dereference_unwrapped->
subtype();
219 if(dereference_unwrapped->
id() == ID_empty)
223 else if(dereference_unwrapped->
id() == ID_pointer &&
224 object_unwrapped->
id() != ID_pointer)
227 std::cout <<
"value_set_dereference: the dereference type has " 228 "too many ID_pointer levels" 230 std::cout <<
" object_type: " << object_type.
pretty() << std::endl;
231 std::cout <<
" dereference_type: " << dereference_type.
pretty()
242 dt_base=
ns.
follow(dereference_type);
244 if(ot_base.
id()==ID_struct &&
245 dt_base.id()==ID_struct)
253 if(dereference_type.
id()==ID_code &&
254 object_type.
id()==ID_code)
258 if((dereference_type.
id()==ID_signedbv ||
259 dereference_type.
id()==ID_unsignedbv) &&
260 (object_type.
id()==ID_signedbv ||
261 object_type.
id()==ID_unsignedbv) &&
272 const exprt &pointer,
283 "pointer dereference",
291 const exprt &pointer_expr,
294 const typet &dereference_type=
297 if(what.
id()==ID_unknown ||
298 what.
id()==ID_invalid)
304 if(what.
id()!=ID_object_descriptor)
305 throw "unknown points-to: "+what.
id_string();
313 std::cout <<
"O: " <<
format(root_object) <<
'\n';
318 if(root_object.
id() == ID_null_object)
333 "pointer dereference",
334 "NULL pointer", tmp_guard);
341 "pointer dereference",
342 "NULL plus offset pointer", tmp_guard);
346 else if(root_object.
id()==ID_dynamic_object)
372 "pointer dereference",
373 "dynamic object deallocated",
383 tmp_guard.
add(is_malloc_object);
390 "pointer dereference",
391 "dynamic object lower bound", tmp_guard);
401 tmp_guard.
add(is_malloc_object);
408 "pointer dereference",
409 "dynamic object upper bound", tmp_guard);
414 else if(root_object.
id()==ID_integer_address)
430 dereference_type,
ns))
439 result.
value=index_expr;
476 equal_exprt equality(pointer_expr, object_pointer);
497 exprt root_object_subexpression=root_object;
507 if(object_type!=
ns.
follow(dereference_type))
510 else if(root_object_type.
id()==ID_array &&
527 exprt adjusted_offset;
536 adjusted_offset=offset;
538 else if(element_size<=0)
540 throw "unknown or invalid type size of:\n" +
545 exprt element_size_expr=
549 offset, ID_div, element_size_expr, offset.
type());
559 result.
value=index_expr;
565 root_object_subexpression,
572 result.
value=root_object_subexpression;
594 std::ostringstream msg;
595 msg <<
"memory model not applicable (got `" 597 <<
format(dereference_type) <<
"')";
600 "pointer dereference", msg.str(), tmp_guard);
621 if(symbol_expr.
id()==ID_string_constant)
628 "pointer dereference",
629 "write access to string constant",
633 else if(symbol_expr.
is_nil() ||
634 symbol_expr.
get_bool(ID_C_invalid_object))
639 else if(symbol_expr.
id()==ID_symbol)
651 "pointer dereference",
675 if(array_type.
id()!=ID_array)
676 throw "bounds check expected array type";
691 throw "no zero constant of index type "+
695 inequality(expr.
index(), ID_lt, zero);
698 tmp_guard.add(inequality);
701 name+
" lower bound", tmp_guard);
705 const exprt &size_expr=
708 if(size_expr.
id()==ID_infinity)
718 throw "index array operand of wrong type";
726 tmp_guard.
add(inequality);
729 name+
" upper bound", tmp_guard);
735 return type.
id()==ID_unsignedbv ||
736 type.
id()==ID_signedbv ||
738 type.
id()==ID_fixedbv ||
739 type.
id()==ID_floatbv ||
740 type.
id()==ID_c_enum_tag;
745 const typet &to_type,
765 if(to_type.
id()==ID_fixedbv || to_type.
id()==ID_floatbv ||
777 to_type.
id()==ID_pointer)
790 const typet &to_type,
806 tmp_guard.
add(offset_not_zero);
809 "offset not zero", tmp_guard);
817 const typet &to_type,
824 if(
from_type.id()==ID_code || to_type.
id()==ID_code)
867 "unknown or invalid type size:\n"+
from_type.pretty());
870 to_type.
id()==ID_empty?
873 to_width.is_not_nil(),
874 "unknown or invalid type size:\n"+to_type.
pretty());
876 from_width.
type()==to_width.type(),
877 "type mismatch on result of size_of_expr");
880 if(bound.type()!=offset.
type())
881 bound.make_typecast(offset.
type());
884 offset_upper_bound(offset, ID_gt, bound);
887 tmp_guard.
add(offset_upper_bound);
889 "pointer dereference",
890 "object upper bound", tmp_guard);
901 tmp_guard.
add(offset_lower_bound);
903 "pointer dereference",
904 "object lower bound", tmp_guard);
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
The type of an expression.
irep_idt name
The unique identifier.
exprt size_of_expr(const typet &type, const namespacet &ns)
struct configt::ansi_ct ansi_c
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
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
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
dereference_callbackt & dereference_callback
const irep_idt & get_identifier() const
Fresh auxiliary symbol creation.
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast a generic exprt to an object_descriptor_exprt.
void invalid_pointer(const exprt &expr, const guardt &guard)
const exprt & root_object() const
The trinary if-then-else operator.
mp_integer pointer_offset_bits(const typet &type, const namespacet &ns)
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)
Compute the size of a type in bytes, rounding up to full bytes.
exprt null_object(const exprt &pointer)
void valid_check(const exprt &expr, const guardt &guard, const modet mode)
exprt dynamic_object_upper_bound(const exprt &pointer, const namespacet &ns, const exprt &access_size)
#define INVARIANT(CONDITION, REASON)
static unsigned invalid_counter
const irep_idt & id() const
void bounds_check(const index_exprt &expr, const guardt &guard)
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Expression classes for byte-level operators.
The boolean constant true.
bool memory_model_bytes(exprt &value, const typet &type, const guardt &guard, const exprt &offset)
A generic base class for binary expressions.
bool get_subexpression_at_offset(exprt &result, mp_integer offset, const typet &target_type_raw, const namespacet &ns)
Operator to dereference a pointer.
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
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
const typet & follow(const typet &) const
static bool is_a_bv_type(const typet &type)
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
valuet build_reference_to(const exprt &what, const modet mode, const exprt &pointer, const guardt &guard)
Get a guard and expression to access what under guard.
Operator to return the address of an object.
Various predicates over pointers in programs.
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)
std::size_t get_width() const
static exprt conditional_cast(const exprt &expr, const typet &type)
virtual void get_value_set(const exprt &expr, value_setst::valuest &value_set)=0
exprt malloc_object(const exprt &pointer, const namespacet &ns)
typet type
Type of symbol.
bool is_prefix_of(const struct_typet &other) 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 array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Base class for all expressions.
exprt pointer_offset(const exprt &pointer)
irep_idt get_object_name() const
const source_locationt & source_location() const
bool is_ssa_expr(const exprt &expr)
symbol_tablet & new_symbol_table
const std::string & id_string() const
Expression to hold a symbol (variable)
exprt dynamic_object(const exprt &pointer)
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)
bool memory_model_conversion(exprt &value, const typet &type, const guardt &guard, const exprt &offset)
void make_typecast(const typet &_type)
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
void add(const exprt &expr)
void set(const irep_namet &name, const irep_idt &value)
const bool exclude_null_derefs
Flag indicating whether value_set_dereferencet::dereference should disregard an apparent attempt to d...
bool dereference_type_compare(const typet &object_type, const typet &dereference_type) const
std::string array_name(const namespacet &ns, const exprt &expr)
Return value for build_reference_to; see that method for documentation.