45 id==
"value_set::return_value" ||
46 id==
"value_set::memory")
50 return type.
id() == ID_struct || type.
id() == ID_struct_tag;
56 return !found.has_value() ? nullptr : &(found->get());
73 if(existing_entry.has_value())
103 auto entry=dest.
read().find(n);
105 if(entry==dest.
read().end())
110 else if(!entry->second)
112 else if(offset && *entry->second == *offset)
127 auto &new_offset = dest.
write()[n];
143 display_name = id2string(e.identifier) + e.suffix;
146 else if(e.
identifier ==
"value_set::return_value")
148 display_name =
"RETURN_VALUE" + e.suffix;
154 const symbolt &symbol=ns.lookup(e.identifier);
155 display_name=id2string(symbol.display_name())+e.suffix;
156 identifier=symbol.name;
158 identifier = id2string(e.identifier);
159 display_name = id2string(identifier) + e.suffix;
163 out << indent << display_name <<
" = { ";
167 std::size_t width = 0;
169 for(object_map_dt::const_iterator o_it = object_map.begin();
170 o_it != object_map.end();
173 const exprt &o = object_numbering[o_it->first];
175 std::ostringstream stream;
177 if(o.id() == ID_invalid || o.id() == ID_unknown)
181 stream <<
"<" << format(o) <<
", ";
184 stream << *o_it->second;
188 if(o.type().is_nil())
191 stream <<
", " << format(o.type());
196 const std::string result = stream.str();
198 width += result.size();
200 object_map_dt::const_iterator next(o_it);
203 if(next != object_map.end())
207 out <<
"\n" << std::string(indent.size(),
' ') <<
" ";
219 if(
object.
id()==ID_invalid ||
220 object.
id()==ID_unknown)
232 return std::move(od);
243 for(
const auto &delta_entry : delta_view)
245 if(delta_entry.is_in_both_maps())
248 delta_entry.get_other_map_value().object_map,
249 delta_entry.m.object_map))
252 make_union(existing_entry.object_map, delta_entry.m.object_map);
271 for(
const auto &number_and_offset : src.
read())
275 dest, number_and_offset.first, number_and_offset.second) !=
289 for(object_map_dt::const_iterator it=src.
read().begin();
290 it!=src.
read().end();
306 if(expr.
id()==ID_pointer_offset)
315 for(object_map_dt::const_iterator
316 it=object_map.begin();
317 it!=object_map.end();
326 if(!ptr_offset.has_value())
329 *ptr_offset += *it->second;
331 if(mod && *ptr_offset != previous_offset)
335 previous_offset = *ptr_offset;
356 .map([&](
const object_map_dt::value_type &pair) {
return to_expr(pair); });
362 bool is_simplified)
const
376 const std::string &suffix,
const std::string &field)
381 suffix.compare(1, field.length(), field) == 0 &&
382 (suffix.length() == field.length() + 1 ||
383 suffix[field.length() + 1] ==
'.' ||
384 suffix[field.length() + 1] ==
'[');
388 const std::string &suffix,
const std::string &field)
392 "suffix should start with " + field);
393 return suffix.substr(field.length() + 1);
399 const std::string &suffix,
403 type.
id() != ID_pointer && type.
id() != ID_signedbv &&
404 type.
id() != ID_unsignedbv && type.
id() != ID_array &&
405 type.
id() != ID_struct && type.
id() != ID_struct_tag &&
406 type.
id() != ID_union && type.
id() != ID_union_tag)
415 return std::move(index);
417 const typet &followed_type = type.
id() == ID_struct_tag
419 : type.
id() == ID_union_tag
424 if(followed_type.
id() == ID_struct || followed_type.
id() == ID_union)
431 const irep_idt &first_component_name =
432 struct_union_type.
components().front().get_name();
438 return std::move(index);
445 return std::move(identifier);
453 const std::string &suffix,
454 const typet &original_type,
458 std::cout <<
"GET_VALUE_SET_REC EXPR: " <<
format(expr) <<
"\n";
459 std::cout <<
"GET_VALUE_SET_REC SUFFIX: " << suffix <<
'\n';
464 if(expr.
id()==ID_unknown || expr.
id()==ID_invalid)
468 else if(expr.
id()==ID_index)
473 type.
id() == ID_array,
"operand 0 of index expression must be an array");
476 to_index_expr(expr).array(), dest,
"[]" + suffix, original_type, ns);
478 else if(expr.
id()==ID_member)
483 type.
id() == ID_struct || type.
id() == ID_union,
484 "compound of member expression must be struct or union");
486 const std::string &component_name=
492 "." + component_name + suffix,
496 else if(expr.
id()==ID_symbol)
501 if(entry_index.has_value())
506 else if(expr.
id()==ID_if)
509 to_if_expr(expr).true_case(), dest, suffix, original_type, ns);
511 to_if_expr(expr).false_case(), dest, suffix, original_type, ns);
513 else if(expr.
id()==ID_address_of)
517 else if(expr.
id()==ID_dereference)
523 if(object_map.begin()==object_map.end())
527 for(object_map_dt::const_iterator
528 it1=object_map.begin();
529 it1!=object_map.end();
542 if(expr.
get(ID_value)==ID_NULL &&
543 expr_type.
id()==ID_pointer)
547 else if(expr_type.
id()==ID_unsignedbv ||
548 expr_type.
id()==ID_signedbv)
556 else if(expr.
id()==ID_typecast)
561 const typet &op_type = op.type();
563 if(op_type.
id()==ID_pointer)
568 else if(op_type.
id()==ID_unsignedbv ||
569 op_type.
id()==ID_signedbv)
582 if(tmp.
read().empty())
587 else if(tmp.
read().size()==1 &&
604 expr.
id() == ID_plus || expr.
id() == ID_minus || expr.
id() == ID_bitor ||
605 expr.
id() == ID_bitand || expr.
id() == ID_bitxor ||
606 expr.
id() == ID_bitnand || expr.
id() == ID_bitnor ||
607 expr.
id() == ID_bitxnor)
610 throw expr.
id_string()+
" expected to have at least two operands";
618 expr.
operands().size() == 2 && expr_type.
id() == ID_pointer &&
619 (expr.
id() == ID_plus || expr.
id() == ID_minus))
639 if(pointer_sub_type.
id()==ID_empty)
644 if(!size.has_value() || (*size) == 0)
652 if(expr.
id()==ID_minus)
658 ptr_operand, pointer_expr_set,
"", ptr_operand.
type(), ns);
666 *it, pointer_expr_set,
"", it->type(), ns);
670 for(object_map_dt::const_iterator
671 it=pointer_expr_set.
read().begin();
672 it!=pointer_expr_set.
read().end();
678 if(offset && i.has_value())
683 insert(dest, it->first, offset);
686 else if(expr.
id()==ID_mult)
692 throw expr.
id_string()+
" expected to have at least two operands";
700 *it, pointer_expr_set,
"", it->type(), ns);
703 for(object_map_dt::const_iterator
704 it=pointer_expr_set.
read().begin();
705 it!=pointer_expr_set.
read().end();
713 insert(dest, it->first, offset);
716 else if(expr.
id()==ID_side_effect)
720 if(statement==ID_function_call)
723 throw "unexpected function_call sideeffect";
725 else if(statement==ID_allocate)
729 const typet &dynamic_type=
730 static_cast<const typet &
>(expr.
find(ID_C_cxx_alloc_type));
738 else if(statement==ID_cpp_new ||
739 statement==ID_cpp_new_array)
742 assert(expr_type.
id()==ID_pointer);
753 else if(expr.
id()==ID_struct)
757 struct_components.size() == expr.
operands().size(),
758 "struct expression should have an operand per component");
759 auto component_iter = struct_components.begin();
760 bool found_component =
false;
766 const std::string &component_name =
770 std::string remaining_suffix =
773 found_component =
true;
787 else if(expr.
id()==ID_with)
793 if(expr_type.
id() == ID_struct && !suffix.
empty())
799 std::string remaining_suffix =
802 with_expr.
new_value(), dest, remaining_suffix, original_type, ns);
818 else if(expr_type.
id() == ID_array && !suffix.
empty())
820 std::string new_value_suffix;
822 new_value_suffix = suffix.substr(2);
829 with_expr.
new_value(), dest, new_value_suffix, original_type, ns);
839 else if(expr.
id()==ID_array)
842 std::string new_suffix = suffix;
844 new_suffix = suffix.substr(2);
851 else if(expr.
id()==ID_array_of)
854 std::string new_suffix = suffix;
856 new_suffix = suffix.substr(2);
863 else if(expr.
id()==ID_dynamic_object)
868 const std::string prefix=
869 "value_set::dynamic_object"+
873 const std::string full_name=prefix+suffix;
887 else if(expr.
id()==ID_byte_extract_little_endian ||
888 expr.
id()==ID_byte_extract_big_endian)
894 exprt op1 = byte_extract_expr.
op1();
898 const auto op1_offset = numeric_cast<mp_integer>(op1);
899 const typet &op_type = ns.
follow(byte_extract_expr.op().type());
900 if(op1_offset.has_value() && op_type.
id() == ID_struct)
906 const irep_idt &name = c.get_name();
910 if(!comp_offset.has_value())
912 else if(*comp_offset > *op1_offset)
914 else if(*comp_offset != *op1_offset)
925 if(op_type.
id() == ID_union)
930 const irep_idt &name = c.get_name();
931 member_exprt member(byte_extract_expr.op(), name, c.type());
939 byte_extract_expr.op(), dest, suffix, original_type, ns);
941 else if(expr.
id()==ID_byte_update_little_endian ||
942 expr.
id()==ID_byte_update_big_endian)
949 byte_update_expr.value(), dest, suffix, original_type, ns);
953 else if(expr.
id() == ID_let)
958 value_sett value_set_with_local_definition = *
this;
959 value_set_with_local_definition.
assign(
960 let_expr.symbol(), let_expr.value(), ns,
false,
false);
963 let_expr.where(), dest, suffix, original_type, ns);
972 std::cout <<
"GET_VALUE_SET_REC RESULT:\n";
973 for(
const auto &obj : dest.
read())
976 std::cout <<
" " <<
format(e) <<
"\n";
987 if(src.
id()==ID_typecast)
989 assert(src.
type().
id()==ID_pointer);
1005 for(object_map_dt::const_iterator
1006 it=object_map.
read().begin();
1007 it!=object_map.
read().end();
1018 std::cout <<
"GET_REFERENCE_SET_REC EXPR: " <<
format(expr)
1022 if(expr.
id()==ID_symbol ||
1023 expr.
id()==ID_dynamic_object ||
1024 expr.
id()==ID_string_constant ||
1025 expr.
id()==ID_array)
1027 if(expr.
type().
id()==ID_array &&
1035 else if(expr.
id()==ID_dereference)
1042 for(
const auto &map_entry : dest.
read())
1051 else if(expr.
id()==ID_index)
1054 throw "index expected to have two operands";
1062 array_type.
id() == ID_array,
"index takes array-typed operand");
1069 for(object_map_dt::const_iterator
1070 a_it=object_map.begin();
1071 a_it!=object_map.end();
1076 if(
object.
id()==ID_unknown)
1085 const auto i = numeric_cast<mp_integer>(offset);
1090 else if(i.has_value() && o)
1094 if(!size.has_value() || *size == 0)
1102 insert(dest, deref_index_expr, o);
1108 else if(expr.
id()==ID_member)
1110 const irep_idt &component_name=expr.
get(ID_component_name);
1119 for(object_map_dt::const_iterator
1120 it=object_map.begin();
1121 it!=object_map.end();
1126 if(
object.
id()==ID_unknown)
1137 const typet &final_object_type = ns.
follow(
object.type());
1139 if(final_object_type.
id()==ID_struct ||
1140 final_object_type.
id()==ID_union)
1143 if(ns.
follow(struct_op.
type())!=final_object_type)
1149 insert(dest, member_expr, o);
1158 else if(expr.
id()==ID_if)
1176 std::cout <<
"ASSIGN LHS: " <<
format(lhs) <<
" : "
1178 std::cout <<
"ASSIGN RHS: " <<
format(rhs) <<
" : "
1180 std::cout <<
"--------------------------------------------\n";
1186 if(type.
id() == ID_struct)
1190 const typet &subtype = c.type();
1191 const irep_idt &name = c.get_name();
1194 if(subtype.
id() == ID_code || c.get_is_padding())
1201 if(rhs.
id()==ID_unknown ||
1202 rhs.
id()==ID_invalid)
1207 rhs_member=
exprt(rhs.
id(), subtype);
1213 "value_sett::assign types should match, got: "
1223 assign(lhs_member, rhs_member, ns,
true, add_to_sets);
1227 else if(type.
id()==ID_array)
1232 if(rhs.
id()==ID_unknown ||
1233 rhs.
id()==ID_invalid)
1246 "value_sett::assign types should match, got: "
1250 if(rhs.
id()==ID_array_of)
1259 else if(rhs.
id()==ID_array ||
1260 rhs.
id()==ID_constant)
1264 assign(lhs_index, *o_it, ns, is_simplified, add_to_sets);
1268 else if(rhs.
id()==ID_with)
1275 assign(lhs_index, op0_index, ns, is_simplified, add_to_sets);
1277 lhs_index,
to_with_expr(rhs).new_value(), ns, is_simplified,
true);
1283 assign(lhs_index, rhs_index, ns, is_simplified,
true);
1298 assign_rec(lhs, values_rhs,
"", ns, add_to_sets);
1305 const std::string &suffix,
1310 std::cout <<
"ASSIGN_REC LHS: " <<
format(lhs) <<
'\n';
1311 std::cout <<
"ASSIGN_REC LHS ID: " << lhs.
id() <<
'\n';
1312 std::cout <<
"ASSIGN_REC SUFFIX: " << suffix <<
'\n';
1314 for(object_map_dt::const_iterator it=values_rhs.
read().begin();
1315 it!=values_rhs.
read().end();
1317 std::cout <<
"ASSIGN_REC RHS: " <<
1322 if(lhs.
id()==ID_symbol)
1327 entryt{identifier, suffix}, lhs.
type(), values_rhs, add_to_sets);
1329 else if(lhs.
id()==ID_dynamic_object)
1334 const std::string name=
1335 "value_set::dynamic_object"+
1340 else if(lhs.
id()==ID_dereference)
1343 throw lhs.
id_string()+
" expected to have one operand";
1348 if(reference_set.
read().size()!=1)
1351 for(object_map_dt::const_iterator
1352 it=reference_set.
read().begin();
1353 it!=reference_set.
read().end();
1360 if(
object.
id()!=ID_unknown)
1361 assign_rec(
object, values_rhs, suffix, ns, add_to_sets);
1364 else if(lhs.
id()==ID_index)
1368 const typet &type = array.type();
1371 type.
id() == ID_array,
"operand 0 of index expression must be an array");
1373 assign_rec(array, values_rhs,
"[]" + suffix, ns,
true);
1375 else if(lhs.
id()==ID_member)
1378 const auto &component_name = lhs_member_expr.get_component_name();
1380 const typet &type = ns.
follow(lhs_member_expr.compound().type());
1383 type.
id() == ID_struct || type.
id() == ID_union,
1384 "operand 0 of member expression must be struct or union");
1387 lhs_member_expr.compound(),
1389 "." +
id2string(component_name) + suffix,
1393 else if(lhs.
id()==
"valid_object" ||
1394 lhs.
id()==
"dynamic_size" ||
1395 lhs.
id()==
"dynamic_type" ||
1396 lhs.
id()==
"is_zero_string" ||
1397 lhs.
id()==
"zero_string" ||
1398 lhs.
id()==
"zero_string_length")
1402 else if(lhs.
id()==ID_string_constant)
1407 else if(lhs.
id() == ID_null_object)
1411 else if(lhs.
id()==ID_typecast)
1415 assign_rec(typecast_expr.
op(), values_rhs, suffix, ns, add_to_sets);
1417 else if(lhs.
id()==ID_byte_extract_little_endian ||
1418 lhs.
id()==ID_byte_extract_big_endian)
1422 else if(lhs.
id()==ID_integer_address)
1428 throw "assign NYI: '" + lhs.
id_string() +
"'";
1446 for(std::size_t i=0; i<arguments.size(); i++)
1448 const std::string identifier=
"value_set::dummy_arg_"+
std::to_string(i);
1449 const symbol_exprt dummy_lhs(identifier, arguments[i].type());
1450 assign(dummy_lhs, arguments[i], ns,
false,
false);
1457 for(code_typet::parameterst::const_iterator
1458 it=parameter_types.begin();
1459 it!=parameter_types.end();
1462 const irep_idt &identifier=it->get_identifier();
1463 if(identifier.
empty())
1470 assign(actual_lhs, v_expr, ns,
true,
true);
1486 assign(lhs, rhs, ns,
false,
false);
1495 if(statement==ID_block)
1500 else if(statement==ID_function_call)
1505 else if(statement==ID_assign)
1508 throw "assignment expected to have two operands";
1512 else if(statement==ID_decl)
1515 throw "decl expected to have one operand";
1519 if(lhs.
id()!=ID_symbol)
1520 throw "decl expected to have symbol on lhs";
1525 lhs_type.
id() == ID_pointer ||
1526 (lhs_type.
id() == ID_array && lhs_type.
subtype().
id() == ID_pointer))
1532 assign(lhs, address_of_expr, ns,
false,
false);
1538 else if(statement==ID_expression)
1542 else if(statement==
"cpp_delete" ||
1543 statement==
"cpp_delete[]")
1547 else if(statement==
"lock" || statement==
"unlock")
1551 else if(statement==ID_asm)
1555 else if(statement==ID_nondet)
1559 else if(statement==ID_printf)
1563 else if(statement==ID_return)
1574 else if(statement==ID_array_set)
1577 else if(statement==ID_array_copy)
1580 else if(statement==ID_array_replace)
1583 else if(statement==ID_assume)
1587 else if(statement==ID_user_specified_predicate ||
1588 statement==ID_user_specified_parameter_predicates ||
1589 statement==ID_user_specified_return_predicates)
1593 else if(statement==ID_fence)
1600 else if(statement==ID_dead)
1607 throw "value_sett: unexpected statement: "+
id2string(statement);
1615 if(expr.
id()==ID_and)
1620 else if(expr.
id()==ID_equal)
1623 else if(expr.
id()==ID_notequal)
1626 else if(expr.
id()==ID_not)
1629 else if(expr.
id()==ID_dynamic_object)
1645 const std::unordered_set<exprt, irep_hash> &values_to_erase)
1647 if(values_to_erase.empty())
1654 std::vector<object_map_dt::key_type> keys_to_erase;
1656 for(
auto &key_value : entry->object_map.read())
1658 const auto &rhs_object =
to_expr(key_value);
1659 if(values_to_erase.count(rhs_object))
1661 keys_to_erase.emplace_back(key_value.first);
1666 keys_to_erase.size() == values_to_erase.size(),
1667 "value_sett::erase_value_from_entry() should erase exactly one value for "
1668 "each element in the set it is given");
1670 entryt replacement = *entry;
1671 for(
const auto &key_to_erase : keys_to_erase)
1680 const std::string &erase_prefix,
1683 for(
const auto &c : struct_union_type.
components())
1685 const typet &subtype = c.type();
1686 const irep_idt &name = c.get_name();
1689 if(subtype.
id() == ID_code || c.get_is_padding())
1698 const std::string &erase_prefix,
1701 if(type.
id() == ID_struct_tag)
1704 else if(type.
id() == ID_union_tag)
1707 else if(type.
id() == ID_array)
optionalt< symbol_exprt > get_failed_symbol(const symbol_exprt &expr, const namespacet &ns)
Get the failed-dereference symbol for the given symbol.
Expression classes for byte-level operators.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
bitvector_typet index_type()
unsignedbv_typet unsigned_char_type()
bitvector_typet char_type()
Operator to return the address of an object.
codet representation of a "return from a function" statement.
const exprt & return_value() const
bool has_return_value() const
std::vector< parametert > parameterst
const parameterst & parameters() const
Data structure for representing an arbitrary statement in a program.
const irep_idt & get_statement() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Representation of heap-allocated objects.
Base class for all expressions.
std::vector< exprt > operandst
bool is_zero() const
Return whether the expression is a constant representing 0.
typet & type()
Return the type of the expression.
bool is_constant() const
Return whether the expression is a constant.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const std::string & get_string(const irep_namet &name) const
const irept & find(const irep_namet &name) const
const std::string & id_string() const
const irep_idt & id() const
const irep_idt & get(const irep_namet &name) const
Extract member of struct or union.
const exprt & compound() const
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Split an expression into a base object and a (byte) offset.
void insert(const key_type &k, valueU &&m)
Insert element, element must not exist in map.
void iterate(std::function< void(const key_type &k, const mapped_type &m)> f) const
Call a function for every key-value pair in the map.
void erase(const key_type &k)
Erase element, element must exist in map.
bool has_key(const key_type &k) const
Check if key is in map.
void replace(const key_type &k, valueU &&m)
Replace element, element must exist in map.
std::vector< delta_view_itemt > delta_viewt
Delta view of the key-value pairs in two maps.
optionalt< std::reference_wrapper< const mapped_type > > find(const key_type &k) const
Find element.
void get_delta_view(const sharing_mapt &other, delta_viewt &delta_view, const bool only_common=true) const
Get a delta view of the elements in the map.
void update(const key_type &k, std::function< void(mapped_type &)> mutator)
Update an element in place; element must exist in map.
const irep_idt & get_statement() const
Structure type, corresponds to C style structs.
Base type for structs and unions.
const typet & component_type(const irep_idt &component_name) const
const componentst & components() const
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
typet type
Type of symbol.
The Boolean constant true.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
const typet & subtype() const
std::list< exprt > valuest
State type in value_set_domaint, used in value-set analysis and goto-symex.
virtual void apply_code_rec(const codet &code, const namespacet &ns)
Subclass customisation point for applying code to this domain:
optionalt< irep_idt > get_index_of_symbol(irep_idt identifier, const typet &type, const std::string &suffix, const namespacet &ns) const
Get the index of the symbol and suffix.
bool eval_pointer_offset(exprt &expr, const namespacet &ns) const
Tries to resolve any pointer_offset_exprt expressions in expr to constant integers using this value-s...
const entryt * find_entry(const irep_idt &id) const
Finds an entry in this value-set.
std::vector< exprt > get_value_set(exprt expr, const namespacet &ns) const
Gets values pointed to by expr, including following dereference operators (i.e.
void output(std::ostream &out, const std::string &indent="") const
Pretty-print this value-set.
void dereference_rec(const exprt &src, exprt &dest) const
Sets dest to src with any wrapping typecasts removed.
void erase_symbol(const symbol_exprt &symbol_expr, const namespacet &ns)
valuest values
Stores the LHS ID -> RHS expression set map.
unsigned location_number
Matches the location_number field of the instruction that corresponds to this value_sett instance in ...
static object_numberingt object_numbering
Global shared object numbering, used to abbreviate expressions stored in value sets.
bool insert(object_mapt &dest, const object_map_dt::value_type &it) const
Merges an existing element into an object map.
void erase_struct_union_symbol(const struct_union_typet &struct_union_type, const std::string &erase_prefix, const namespacet &ns)
void get_reference_set_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
See get_reference_set.
exprt to_expr(const object_map_dt::value_type &it) const
Converts an object_map_dt element object_number -> offset into an object_descriptor_exprt with ....
void erase_values_from_entry(const irep_idt &index, const std::unordered_set< exprt, irep_hash > &values_to_erase)
Update the entry stored at index by erasing any values listed in values_to_erase.
void update_entry(const entryt &e, const typet &type, const object_mapt &new_values, bool add_to_sets)
Adds or replaces an entry in this value-set.
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns, bool is_simplified, bool add_to_sets)
Transforms this value-set by executing executing the assignment lhs := rhs against it.
virtual void assign_rec(const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, bool add_to_sets)
Subclass customisation point for recursion over LHS expression:
insert_actiont get_insert_action(const object_mapt &dest, object_numberingt::number_type n, const offsett &offset) const
Determines what would happen if object number n was inserted into map dest with offset offset – the p...
bool make_union(object_mapt &dest, const object_mapt &src) const
Merges two RHS expression sets.
virtual bool field_sensitive(const irep_idt &id, const typet &type)
Determines whether an identifier of a given type should have its fields distinguished.
optionalt< mp_integer > offsett
Represents the offset into an object: either a unique integer offset, or an unknown value,...
void guard(const exprt &expr, const namespacet &ns)
Transforms this value-set by assuming an expression holds.
bool make_union_would_change(const object_mapt &dest, const object_mapt &src) const
Determines whether merging two RHS expression sets would cause any change.
void do_end_function(const exprt &lhs, const namespacet &ns)
Transforms this value-set by assigning this function's return value to a given LHS expression.
static const object_map_dt empty_object_map
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
Transforms this value-set by executing the actual -> formal parameter assignments for a particular ca...
virtual void get_value_set_rec(const exprt &expr, object_mapt &dest, const std::string &suffix, const typet &original_type, const namespacet &ns) const
Subclass customisation point for recursion over RHS expression:
void get_reference_set(const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const
Gets the set of expressions that expr may refer to, according to this value set.
virtual void apply_assign_side_effects(const exprt &lhs, const exprt &rhs, const namespacet &)
Subclass customisation point to apply global side-effects to this domain, after RHS values are read b...
std::map< object_numberingt::number_type, offsett > object_map_dt
Represents a set of expressions (exprt instances) with corresponding offsets (offsett instances).
virtual void adjust_assign_rhs_values(const exprt &rhs, const namespacet &, object_mapt &rhs_values) const
Subclass customisation point to filter or otherwise alter the value-set returned from get_value_set b...
void erase_symbol_rec(const typet &type, const std::string &erase_prefix, const namespacet &ns)
Operator to update elements in structs and arrays.
bool has_prefix(const std::string &s, const std::string &prefix)
#define forall_operands(it, expr)
#define Forall_operands(it, expr)
const std::string & id2string(const irep_idt &d)
nonstd::optional< T > optionalt
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
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.
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
optionalt< mp_integer > compute_pointer_offset(const exprt &expr, const namespacet &ns)
exprt dynamic_object(const exprt &pointer)
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const code_returnt & to_code_return(const codet &code)
bool can_cast_expr< code_inputt >(const exprt &base)
side_effect_exprt & to_side_effect_expr(exprt &expr)
const code_assumet & to_code_assume(const codet &code)
bool can_cast_expr< code_outputt >(const exprt &base)
const codet & to_code(const exprt &expr)
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Represents a row of a value_sett.
static bool failed(bool error_indicator)
static std::string strip_first_field_from_suffix(const std::string &suffix, const std::string &field)
static bool suffix_starts_with_field(const std::string &suffix, const std::string &field)
Check if 'suffix' starts with 'field'.