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();
110 values.push_back(value);
124 for(std::list<valuet>::const_iterator
128 if(it->value.is_nil())
140 pointer, failed_symbol))
144 failure_value.
set(ID_C_invalid_object,
true);
161 failure_value.
set(ID_C_invalid_object,
true);
165 value.
value=failure_value;
167 values.push_front(value);
174 for(std::list<valuet>::const_iterator
179 if(it->value.is_not_nil())
184 value=
if_exprt(it->pointer_guard, it->value, value);
189 std::cout <<
"R: " <<
format(value) <<
"\n\n";
196 const typet &object_type,
197 const typet &dereference_type)
const 207 const typet *object_unwrapped = &object_type;
208 const typet *dereference_unwrapped = &dereference_type;
209 while(object_unwrapped->
id() == ID_pointer &&
210 dereference_unwrapped->
id() == ID_pointer)
212 object_unwrapped = &object_unwrapped->
subtype();
213 dereference_unwrapped = &dereference_unwrapped->
subtype();
215 if(dereference_unwrapped->
id() == ID_empty)
219 else if(dereference_unwrapped->
id() == ID_pointer &&
220 object_unwrapped->
id() != ID_pointer)
223 std::cout <<
"value_set_dereference: the dereference type has " 224 "too many ID_pointer levels" 226 std::cout <<
" object_type: " << object_type.
pretty() << std::endl;
227 std::cout <<
" dereference_type: " << dereference_type.
pretty()
238 dt_base=
ns.
follow(dereference_type);
240 if(ot_base.
id()==ID_struct &&
241 dt_base.id()==ID_struct)
249 if(dereference_type.
id()==ID_code &&
250 object_type.
id()==ID_code)
254 if((dereference_type.
id()==ID_signedbv ||
255 dereference_type.
id()==ID_unsignedbv) &&
256 (object_type.
id()==ID_signedbv ||
257 object_type.
id()==ID_unsignedbv) &&
268 const exprt &pointer,
279 "pointer dereference",
287 const exprt &pointer_expr,
290 const typet &dereference_type=
293 if(what.
id()==ID_unknown ||
294 what.
id()==ID_invalid)
300 if(what.
id()!=ID_object_descriptor)
301 throw "unknown points-to: "+what.
id_string();
309 std::cout <<
"O: " <<
format(root_object) <<
'\n';
314 if(root_object.
id() == ID_null_object)
325 "pointer dereference",
326 "NULL pointer", tmp_guard);
333 "pointer dereference",
334 "NULL plus offset pointer", tmp_guard);
338 else if(root_object.
id()==ID_dynamic_object)
364 "pointer dereference",
365 "dynamic object deallocated",
375 tmp_guard.
add(is_malloc_object);
382 "pointer dereference",
383 "dynamic object lower bound", tmp_guard);
393 tmp_guard.
add(is_malloc_object);
401 "pointer dereference",
402 "dynamic object upper bound", tmp_guard);
407 else if(root_object.
id()==ID_integer_address)
423 dereference_type,
ns))
432 result.
value=index_expr;
469 equal_exprt equality(pointer_expr, object_pointer);
490 exprt root_object_subexpression=root_object;
500 if(object_type!=
ns.
follow(dereference_type))
503 else if(root_object_type.
id()==ID_array &&
520 exprt adjusted_offset;
529 adjusted_offset=offset;
531 else if(element_size<=0)
533 throw "unknown or invalid type size of:\n" +
538 exprt element_size_expr=
542 offset, ID_div, element_size_expr, offset.
type());
552 result.
value=index_expr;
558 root_object_subexpression,
565 result.
value=root_object_subexpression;
587 std::ostringstream msg;
588 msg <<
"memory model not applicable (got `" 590 <<
format(dereference_type) <<
"')";
593 "pointer dereference", msg.str(), tmp_guard);
614 if(symbol_expr.
id()==ID_string_constant)
621 "pointer dereference",
622 "write access to string constant",
626 else if(symbol_expr.
is_nil() ||
627 symbol_expr.
get_bool(ID_C_invalid_object))
632 else if(symbol_expr.
id()==ID_symbol)
644 "pointer dereference",
668 if(array_type.
id()!=ID_array)
669 throw "bounds check expected array type";
684 throw "no zero constant of index type "+
688 inequality(expr.
index(), ID_lt, zero);
691 tmp_guard.add(inequality);
694 name+
" lower bound", tmp_guard);
698 const exprt &size_expr=
701 if(size_expr.
id()==ID_infinity)
711 throw "index array operand of wrong type";
719 tmp_guard.
add(inequality);
722 name+
" upper bound", tmp_guard);
728 return type.
id()==ID_unsignedbv ||
729 type.
id()==ID_signedbv ||
731 type.
id()==ID_fixedbv ||
732 type.
id()==ID_floatbv ||
733 type.
id()==ID_c_enum_tag;
738 const typet &to_type,
758 if(to_type.
id()==ID_fixedbv || to_type.
id()==ID_floatbv ||
770 to_type.
id()==ID_pointer)
783 const typet &to_type,
799 tmp_guard.
add(offset_not_zero);
802 "offset not zero", tmp_guard);
810 const typet &to_type,
817 if(
from_type.id()==ID_code || to_type.
id()==ID_code)
860 "unknown or invalid type size:\n"+
from_type.pretty());
863 to_type.
id()==ID_empty?
866 to_width.is_not_nil(),
867 "unknown or invalid type size:\n"+to_type.
pretty());
869 from_width.
type()==to_width.type(),
870 "type mismatch on result of size_of_expr");
873 if(bound.type()!=offset.
type())
874 bound.make_typecast(offset.
type());
877 offset_upper_bound(offset, ID_gt, bound);
880 tmp_guard.
add(offset_upper_bound);
882 "pointer dereference",
883 "object upper bound", tmp_guard);
894 tmp_guard.
add(offset_lower_bound);
896 "pointer dereference",
897 "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)
#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.
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.
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
exprt dynamic_object_upper_bound(const exprt &pointer, const typet &dereference_type, const namespacet &ns, const exprt &access_size)
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)
bool dereference_type_compare(const typet &object_type, const typet &dereference_type) const
std::string array_name(const namespacet &ns, const exprt &expr)