46 id==
"value_set::return_value" ||
47 id==
"value_set::memory")
51 return ns.
follow(type).
id()==ID_struct;
66 std::pair<valuest::iterator, bool>
r=
67 values.insert(std::pair<idt, entryt>(index, e));
69 return r.first->second;
82 dest.
write()[n] = offset;
85 else if(!entry->second)
87 else if(offset && *entry->second == *offset)
91 dest.
write()[n].reset();
98 std::ostream &out)
const 100 for(valuest::const_iterator
107 const entryt &e=v_it->second;
114 else if(e.
identifier==
"value_set::return_value")
116 display_name=
"RETURN_VALUE"+e.
suffix;
124 identifier=symbol.
name;
140 o_it=object_map.
begin();
141 o_it!=object_map.
end();
148 if(o.
id()==ID_invalid || o.
id()==ID_unknown)
152 result=
"<"+
from_expr(ns, identifier, o)+
", ";
169 width+=result.size();
174 if(next!=object_map.
end())
190 if(
object.
id()==ID_invalid ||
191 object.
id()==ID_unknown)
210 valuest::iterator v_it=
values.begin();
212 for(valuest::const_iterator
213 it=new_values.begin();
214 it!=new_values.end();
217 if(v_it==
values.end() || it->first<v_it->first)
224 else if(v_it->first<it->first)
230 assert(v_it->first==it->first);
233 const entryt &new_e=it->second;
266 if(expr.
id()==ID_pointer_offset)
278 it=object_map.
begin();
279 it!=object_map.
end();
291 ptr_offset += *it->second;
293 if(mod && ptr_offset!=previous_offset)
297 previous_offset=ptr_offset;
328 for(value_setst::valuest::const_iterator it=dest.begin();
329 it!=dest.end(); it++)
330 std::cout <<
"GET_VALUE_SET: " <<
format(*it) <<
'\n';
338 bool is_simplified)
const 351 const std::string &suffix,
const std::string &field)
356 suffix.compare(1, field.length(), field) == 0 &&
357 (suffix.length() == field.length() + 1 ||
358 suffix[field.length() + 1] ==
'.' ||
359 suffix[field.length() + 1] ==
'[');
363 const std::string &suffix,
const std::string &field)
367 "suffix should start with " + field);
368 return suffix.substr(field.length() + 1);
374 const std::string &suffix,
375 const typet &original_type,
379 std::cout <<
"GET_VALUE_SET_REC EXPR: " <<
format(expr) <<
"\n";
380 std::cout <<
"GET_VALUE_SET_REC SUFFIX: " << suffix <<
'\n';
385 if(expr.
id()==ID_unknown || expr.
id()==ID_invalid)
389 else if(expr.
id()==ID_index)
396 type.id()==ID_incomplete_array,
397 "operand 0 of index expression must be an array");
401 else if(expr.
id()==ID_member)
408 type.id()==ID_union ||
409 type.id()==ID_incomplete_struct ||
410 type.id()==ID_incomplete_union,
411 "operand 0 of member expression must be struct or union");
413 const std::string &component_name=
417 "."+component_name+suffix, original_type, ns);
419 else if(expr.
id()==ID_symbol)
424 if(expr_type.
id()==ID_pointer ||
425 expr_type.
id()==ID_signedbv ||
426 expr_type.
id()==ID_unsignedbv ||
427 expr_type.
id()==ID_struct ||
428 expr_type.
id()==ID_union ||
429 expr_type.
id()==ID_array)
432 valuest::const_iterator v_it=
437 (expr_type.
id()==ID_struct ||
438 expr_type.
id()==ID_union))
443 const std::string first_component_name=
444 struct_union_type.
components().front().get_string(ID_name);
447 id2string(identifier)+
"."+first_component_name+suffix);
452 v_it=
values.find(identifier);
462 else if(expr.
id()==ID_if)
465 throw "if takes three operands";
470 else if(expr.
id()==ID_address_of)
473 throw expr.
id_string()+
" expected to have one operand";
477 else if(expr.
id()==ID_dereference)
483 if(object_map.
begin()==object_map.
end())
488 it1=object_map.
begin();
489 it1!=object_map.
end();
499 else if(expr.
id()==
"reference_to")
508 if(object_map.
begin()==object_map.
end())
513 it=object_map.
begin();
514 it!=object_map.
end();
527 if(expr.
get(ID_value)==ID_NULL &&
528 expr_type.
id()==ID_pointer)
532 else if(expr_type.
id()==ID_unsignedbv ||
533 expr_type.
id()==ID_signedbv)
541 else if(expr.
id()==ID_typecast)
544 throw "typecast takes one operand";
550 if(op_type.
id()==ID_pointer)
555 else if(op_type.
id()==ID_unsignedbv ||
556 op_type.
id()==ID_signedbv)
590 else if(expr.
id()==ID_plus ||
594 throw expr.
id_string()+
" expected to have at least two operands";
603 expr_type.
id()==ID_pointer)
611 ptr_operand=expr.
op1();
616 ptr_operand=expr.
op0();
622 if(pointer_sub_type.
id()==ID_empty)
635 if(expr.
id()==ID_minus)
641 ptr_operand, pointer_expr_set,
"", ptr_operand.
type(), ns);
649 *it, pointer_expr_set,
"", it->type(), ns);
655 it!=pointer_expr_set.
read().
end();
661 if(offset && i_is_set)
666 insert(dest, it->first, offset);
669 else if(expr.
id()==ID_mult)
675 throw expr.
id_string()+
" expected to have at least two operands";
683 *it, pointer_expr_set,
"", it->type(), ns);
688 it!=pointer_expr_set.
read().
end();
696 insert(dest, it->first, offset);
699 else if(expr.
id()==ID_side_effect)
703 if(statement==ID_function_call)
706 throw "unexpected function_call sideeffect";
708 else if(statement==ID_allocate)
712 const typet &dynamic_type=
713 static_cast<const typet &
>(expr.
find(ID_C_cxx_alloc_type));
721 else if(statement==ID_cpp_new ||
722 statement==ID_cpp_new_array)
725 assert(expr_type.
id()==ID_pointer);
736 else if(expr.
id()==ID_struct)
740 struct_components.size() == expr.
operands().size(),
741 "struct expression should have an operand per component");
742 auto component_iter = struct_components.begin();
743 bool found_component =
false;
749 const std::string &component_name =
753 std::string remaining_suffix =
756 found_component =
true;
770 else if(expr.
id()==ID_with)
776 if(expr_type.
id() == ID_struct && !suffix.
empty())
782 std::string remaining_suffix =
785 with_expr.
new_value(), dest, remaining_suffix, original_type, ns);
801 else if(expr_type.
id() == ID_array && !suffix.
empty())
803 std::string new_value_suffix;
805 new_value_suffix = suffix.substr(2);
812 with_expr.
new_value(), dest, new_value_suffix, original_type, ns);
822 else if(expr.
id()==ID_array)
825 std::string new_suffix = suffix;
827 new_suffix = suffix.substr(2);
834 else if(expr.
id()==ID_array_of)
837 std::string new_suffix = suffix;
839 new_suffix = suffix.substr(2);
846 else if(expr.
id()==ID_dynamic_object)
851 const std::string prefix=
852 "value_set::dynamic_object"+
856 const std::string full_name=prefix+suffix;
859 valuest::const_iterator v_it=
values.find(full_name);
870 else if(expr.
id()==ID_byte_extract_little_endian ||
871 expr.
id()==ID_byte_extract_big_endian)
874 throw "byte_extract takes two operands";
884 if(!
to_integer(op1, op1_offset) && op0_type.
id()==ID_struct)
888 for(struct_union_typet::componentst::const_iterator
890 !found && c_it!=struct_type.
components().end();
893 const irep_idt &name=c_it->get_name();
897 if(comp_offset>op1_offset)
899 else if(comp_offset!=op1_offset)
909 if(op0_type.
id()==ID_union)
914 for(union_typet::componentst::const_iterator
918 const irep_idt &name=c_it->get_name();
928 else if(expr.
id()==ID_byte_update_little_endian ||
929 expr.
id()==ID_byte_update_big_endian)
932 throw "byte_update takes three operands";
943 std::cout <<
"WARNING: not doing " << expr.
id() <<
'\n';
948 std::cout <<
"GET_VALUE_SET_REC RESULT:\n";
949 for(
const auto &obj : dest.
read())
952 std::cout <<
" " <<
format(e) <<
"\n";
963 if(src.
id()==ID_typecast)
965 assert(src.
type().
id()==ID_pointer);
968 throw "typecast expects one operand";
997 std::cout <<
"GET_REFERENCE_SET_REC EXPR: " <<
format(expr)
1001 if(expr.
id()==ID_symbol ||
1002 expr.
id()==ID_dynamic_object ||
1003 expr.
id()==ID_string_constant ||
1004 expr.
id()==ID_array)
1006 if(expr.
type().
id()==ID_array &&
1014 else if(expr.
id()==ID_dereference)
1017 throw expr.
id_string()+
" expected to have one operand";
1022 for(expr_sett::const_iterator it=value_set.begin();
1023 it!=value_set.end(); it++)
1024 std::cout <<
"VALUE_SET: " <<
format(*it) <<
'\n';
1029 else if(expr.
id()==ID_index)
1032 throw "index expected to have two operands";
1039 assert(array_type.
id()==ID_array ||
1040 array_type.
id()==ID_incomplete_array);
1048 a_it=object_map.
begin();
1049 a_it!=object_map.
end();
1054 if(
object.
id()==ID_unknown)
1059 index_expr.
array()=object;
1063 if(ns.
follow(
object.type())!=array_type)
1084 insert(dest, index_expr, o);
1090 else if(expr.
id()==ID_member)
1092 const irep_idt &component_name=expr.
get(ID_component_name);
1095 throw "member expected to have one operand";
1105 it=object_map.
begin();
1106 it!=object_map.
end();
1111 if(
object.
id()==ID_unknown)
1122 const typet &final_object_type = ns.
follow(
object.type());
1124 if(final_object_type.id()==ID_struct ||
1125 final_object_type.id()==ID_union)
1128 if(ns.
follow(struct_op.
type())!=final_object_type)
1129 member_expr.op0().make_typecast(struct_op.
type());
1131 insert(dest, member_expr, o);
1140 else if(expr.
id()==ID_if)
1143 throw "if takes three operands";
1161 std::cout <<
"ASSIGN LHS: " <<
format(lhs) <<
" : " 1163 std::cout <<
"ASSIGN RHS: " <<
format(rhs) <<
" : " 1165 std::cout <<
"--------------------------------------------\n";
1171 if(type.
id()==ID_struct ||
1172 type.
id()==ID_union)
1177 for(struct_union_typet::componentst::const_iterator
1182 const typet &subtype=c_it->type();
1183 const irep_idt &name=c_it->get(ID_name);
1186 if(subtype.
id()==ID_code ||
1187 c_it->get_is_padding())
continue;
1193 if(rhs.
id()==ID_unknown ||
1194 rhs.
id()==ID_invalid)
1196 rhs_member=
exprt(rhs.
id(), subtype);
1201 throw "value_sett::assign type mismatch: " 1207 assign(lhs_member, rhs_member, ns, is_simplified, add_to_sets);
1211 else if(type.
id()==ID_array)
1216 if(rhs.
id()==ID_unknown ||
1217 rhs.
id()==ID_invalid)
1229 throw "value_sett::assign type mismatch: " 1233 if(rhs.
id()==ID_array_of)
1236 assign(lhs_index, rhs.
op0(), ns, is_simplified, add_to_sets);
1238 else if(rhs.
id()==ID_array ||
1239 rhs.
id()==ID_constant)
1243 assign(lhs_index, *o_it, ns, is_simplified, add_to_sets);
1247 else if(rhs.
id()==ID_with)
1254 assign(lhs_index, op0_index, ns, is_simplified, add_to_sets);
1255 assign(lhs_index, rhs.
op2(), ns, is_simplified,
true);
1261 assign(lhs_index, rhs_index, ns, is_simplified,
true);
1277 assign_rec(lhs, values_rhs,
"", ns, add_to_sets);
1286 if(op.
type().
id()!=ID_pointer)
1287 throw "free expected to have pointer-type operand";
1299 it=object_map.
begin();
1300 it!=object_map.
end();
1305 if(
object.
id()==ID_dynamic_object)
1317 for(valuest::iterator v_it=
values.begin();
1324 v_it->second.object_map.read();
1329 o_it=old_object_map.
begin();
1330 o_it!=old_object_map.
end();
1335 if(
object.
id()==ID_dynamic_object)
1341 set(new_object_map, *o_it);
1348 insert(new_object_map, tmp, o);
1353 set(new_object_map, *o_it);
1357 v_it->second.object_map=new_object_map;
1364 const std::string &suffix,
1369 std::cout <<
"ASSIGN_REC LHS: " <<
format(lhs) <<
'\n';
1370 std::cout <<
"ASSIGN_REC LHS ID: " << lhs.
id() <<
'\n';
1371 std::cout <<
"ASSIGN_REC SUFFIX: " << suffix <<
'\n';
1376 std::cout <<
"ASSIGN_REC RHS: " <<
1381 if(lhs.
id()==ID_symbol)
1392 else if(lhs.
id()==ID_dynamic_object)
1397 const std::string name=
1398 "value_set::dynamic_object"+
1405 else if(lhs.
id()==ID_dereference)
1408 throw lhs.
id_string()+
" expected to have one operand";
1418 it!=reference_set.
read().
end();
1425 if(
object.
id()!=ID_unknown)
1426 assign_rec(
object, values_rhs, suffix, ns, add_to_sets);
1429 else if(lhs.
id()==ID_index)
1432 throw "index expected to have two operands";
1437 "operand 0 of index expression must be an array");
1441 else if(lhs.
id()==ID_member)
1444 throw "member expected to have one operand";
1446 const std::string &component_name=lhs.
get_string(ID_component_name);
1451 type.
id()==ID_union ||
1452 type.
id()==ID_incomplete_struct ||
1453 type.
id()==ID_incomplete_union,
1454 "operand 0 of member expression must be struct or union");
1457 lhs.
op0(), values_rhs,
"."+component_name+suffix, ns, add_to_sets);
1459 else if(lhs.
id()==
"valid_object" ||
1460 lhs.
id()==
"dynamic_size" ||
1461 lhs.
id()==
"dynamic_type" ||
1462 lhs.
id()==
"is_zero_string" ||
1463 lhs.
id()==
"zero_string" ||
1464 lhs.
id()==
"zero_string_length")
1468 else if(lhs.
id()==ID_string_constant)
1473 else if(lhs.
id() == ID_null_object)
1477 else if(lhs.
id()==ID_typecast)
1481 assign_rec(typecast_expr.
op(), values_rhs, suffix, ns, add_to_sets);
1483 else if(lhs.
id()==ID_byte_extract_little_endian ||
1484 lhs.
id()==ID_byte_extract_big_endian)
1489 else if(lhs.
id()==ID_integer_address)
1495 throw "assign NYI: `"+lhs.
id_string()+
"'";
1513 for(std::size_t i=0; i<arguments.size(); i++)
1515 const std::string identifier=
"value_set::dummy_arg_"+
std::to_string(i);
1516 const symbol_exprt dummy_lhs(identifier, arguments[i].type());
1517 assign(dummy_lhs, arguments[i], ns,
false,
false);
1524 for(code_typet::parameterst::const_iterator
1525 it=parameter_types.begin();
1526 it!=parameter_types.end();
1529 const irep_idt &identifier=it->get_identifier();
1537 assign(actual_lhs, v_expr, ns,
true,
true);
1553 assign(lhs, rhs, ns,
false,
false);
1562 if(statement==ID_block)
1567 else if(statement==ID_function_call)
1572 else if(statement==ID_assign ||
1576 throw "assignment expected to have two operands";
1580 else if(statement==ID_decl)
1583 throw "decl expected to have one operand";
1587 if(lhs.
id()!=ID_symbol)
1588 throw "decl expected to have symbol on lhs";
1592 if(lhs_type.
id()==ID_pointer ||
1593 (lhs_type.
id()==ID_array &&
1603 assign(lhs, address_of_expr, ns,
false,
false);
1609 else if(statement==ID_expression)
1613 else if(statement==
"cpp_delete" ||
1614 statement==
"cpp_delete[]")
1618 else if(statement==ID_free)
1623 throw "free expected to have one operand";
1627 else if(statement==
"lock" || statement==
"unlock")
1631 else if(statement==ID_asm)
1635 else if(statement==ID_nondet)
1639 else if(statement==ID_printf)
1643 else if(statement==ID_return)
1649 assign(lhs, code.
op0(), ns,
false,
false);
1652 else if(statement==ID_array_set)
1655 else if(statement==ID_array_copy)
1658 else if(statement==ID_array_replace)
1661 else if(statement==ID_assume)
1665 else if(statement==ID_user_specified_predicate ||
1666 statement==ID_user_specified_parameter_predicates ||
1667 statement==ID_user_specified_return_predicates)
1671 else if(statement==ID_fence)
1674 else if(statement==ID_input || statement==ID_output)
1678 else if(statement==ID_dead)
1685 throw "value_sett: unexpected statement: "+
id2string(statement);
1693 if(expr.
id()==ID_and)
1698 else if(expr.
id()==ID_equal)
1701 else if(expr.
id()==ID_notequal)
1704 else if(expr.
id()==ID_not)
1707 else if(expr.
id()==ID_dynamic_object)
1719 assign(expr.
op0(), address_of, ns,
false,
false);
1731 if(src.
id()==ID_struct ||
1732 src.
id()==ID_constant)
1738 else if(src.
id()==ID_with)
1743 const exprt &member_operand=src.
op1();
1745 if(component_name==member_operand.get(ID_component_name))
1752 else if(src.
id()==ID_typecast)
1761 member_exprt member_expr(src, component_name, subtype);
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...
const irep_idt & get_statement() const
The type of an expression.
irep_idt name
The unique identifier.
const std::string & id2string(const irep_idt &d)
Represents a row of a value_sett.
const std::string integer2string(const mp_integer &n, unsigned base)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const code_assumet & to_code_assume(const codet &code)
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast a generic exprt to a dynamic_object_exprt.
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
static bool suffix_starts_with_field(const std::string &suffix, const std::string &field)
Check if 'suffix' starts with 'field'.
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
const irep_idt & get_identifier() const
mp_integer member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
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...
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
bool make_union(object_mapt &dest, const object_mapt &src) const
Merges two RHS expression sets.
virtual void apply_code_rec(const codet &code, const namespacet &ns)
Subclass customisation point for applying code to this domain:
std::vector< parametert > parameterst
void get_reference_set_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
See get_reference_set.
void get_value_set(const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const
Gets values pointed to by expr, including following dereference operators (i.e.
const componentst & components() const
static const object_map_dt blank
static object_numberingt object_numbering
Global shared object numbering, used to abbreviate expressions stored in value sets.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
void dereference_rec(const exprt &src, exprt &dest) const
Sets dest to src with any wrapping typecasts removed.
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...
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:
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
static std::string strip_first_field_from_suffix(const std::string &suffix, const std::string &field)
#define INVARIANT(CONDITION, REASON)
Extract member of struct or union.
static bool field_sensitive(const irep_idt &id, const typet &type, const namespacet &)
const irep_idt & id() const
The boolean constant true.
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...
exprt get_failed_symbol(const symbol_exprt &expr, const namespacet &ns)
Get the failed-dereference symbol for the given symbol.
data_typet::value_type value_type
const irep_idt & get(const irep_namet &name) const
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...
bool has_prefix(const std::string &s, const std::string &prefix)
data_typet::const_iterator const_iterator
split an expression into a base object and a (byte) offset
optionalt< mp_integer > offsett
Represents the offset into an object: either a unique integer offset, or an unknown value...
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:
#define forall_operands(it, expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
const typet & follow(const typet &) const
bitvector_typet index_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...
typename Map::mapped_type number_type
typet component_type(const irep_idt &component_name) const
Operator to return the address of an object.
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
bool has_component(const irep_idt &component_name) const
std::vector< exprt > operandst
const irep_idt & display_name() const
mp_integer compute_pointer_offset(const exprt &expr, const namespacet &ns)
const_iterator find(T &&t) const
bool insert(object_mapt &dest, const object_map_dt::value_type &it) const
Merges an existing entry into an object map.
std::unordered_map< idt, entryt, string_hash > valuest
Map representing the entire value set, mapping from string LHS IDs to RHS expression sets...
const with_exprt & to_with_expr(const exprt &expr)
Cast a generic exprt to a with_exprt.
typet type
Type of symbol.
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...
Base type of C structs and unions, and C++ classes.
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.
Base class for all expressions.
const parameterst & parameters() const
std::size_t component_number(const irep_idt &component_name) const
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Operator to update elements in structs and arrays.
std::string to_string(const string_constraintt &expr)
Used for debug printing.
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
std::set< unsigned int > dynamic_object_id_sett
Set of dynamic object numbers, equivalent to a set of dynamic_object_exprts with corresponding IDs...
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Represents a set of expressions (exprt instances) with corresponding offsets (offsett instances)...
const std::string & get_string(const irep_namet &name) const
const std::string & id_string() const
#define Forall_operands(it, expr)
const codet & to_code(const exprt &expr)
Expression to hold a symbol (variable)
void output(const namespacet &ns, std::ostream &out) const
Pretty-print this value-set.
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
exprt dynamic_object(const exprt &pointer)
A statement in a programming language.
exprt to_expr(const object_map_dt::value_type &it) const
Converts an object_map_dt entry object_number -> offset into an object_descriptor_exprt with ...
unsignedbv_typet unsigned_char_type()
const typet & subtype() const
entryt & get_entry(const entryt &e, const typet &type, const namespacet &ns)
Gets or inserts an entry in this value-set.
#define DATA_INVARIANT(CONDITION, REASON)
void guard(const exprt &expr, const namespacet &ns)
Transforms this value-set by assuming an expression holds.
void do_free(const exprt &op, const namespacet &ns)
Marks objects that may be pointed to by op as maybe-invalid.
std::list< exprt > valuest
void make_typecast(const typet &_type)
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
const irept & find(const irep_namet &name) const
valuest values
Stores the LHS ID -> RHS expression set map.
bitvector_typet char_type()
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
bool simplify(exprt &expr, const namespacet &ns)
unsigned location_number
Matches the location_number field of the instruction that corresponds to this value_sett instance in ...
exprt make_member(const exprt &src, const irep_idt &component_name, const namespacet &ns)
Extracts a member from a struct- or union-typed expression.