35 #define forall_objects(it, map) \ 36 for(object_map_dt::const_iterator (it)=(map).begin(); \ 40 #define forall_valid_objects(it, map) \ 41 for(object_map_dt::const_iterator (it)=(map).begin(); \ 44 if((map).is_valid_at((it)->first, from_function, from_target_index)) 46 #define Forall_objects(it, map) \ 47 for(object_map_dt::iterator (it)=(map).begin(); \ 51 #define Forall_valid_objects(it, map) \ 52 for(object_map_dt::iterator (it)=(map).begin(); \ 55 if((map).is_valid_at((it)->first, from_function, from_target_index)) 59 std::ostream &out)
const 61 for(valuest::const_iterator
68 const entryt &e=v_it->second;
99 identifier=symbol.
name;
106 out << display_name <<
"={ ";
116 std::string result=
"<";
118 if(o.
id()==ID_invalid)
122 if(o.
type().
id()==ID_unknown)
124 else if(o.
type().
id()==ID_invalid)
130 else if(o.
id()==ID_unknown)
134 if(o.
type().
id()==ID_unknown)
136 else if(o.
type().
id()==ID_invalid)
144 result+=
from_expr(ns, identifier, o)+
", ";
146 if(o_it->second.offset_is_set)
153 if(o.
type().
id()==ID_unknown)
157 if(o.
type().
id()==
"#REF#")
167 out << result <<
'\n';
170 object_map_dt::validity_rangest::const_iterator vr =
175 if(vr->second.empty())
176 std::cout <<
" Empty validity record\n";
179 for(object_map_dt::vrange_listt::const_iterator vit =
181 vit!=vr->second.end();
185 " [" << vit->from <<
"," << vit->to <<
"]";
188 from_target_index<=vit->to)
196 out <<
" No validity information\n";
200 width+=result.size();
205 if(next!=object_map.
read().
end())
227 std::cout <<
"FLATTEN: Done.\n";
235 unsigned at_function,
236 unsigned at_index)
const 243 assert(seen.find(identifier + e.
suffix)==seen.end());
245 bool generalize_index=
false;
246 std::list<const object_map_dt::vrange_listt*> add_ranges;
248 seen.insert(identifier + e.
suffix);
254 if(o.
type().
id()==
"#REF#")
256 if(seen.find(o.
get(ID_identifier))!=seen.end())
258 generalize_index=
true;
260 object_map_dt::validity_rangest::const_iterator vit=
266 add_ranges.push_back(&vl);
271 valuest::const_iterator fi=
values.find(o.
get(ID_identifier));
276 se.
set(ID_identifier, o.
get(ID_identifier));
284 object_map_dt::validity_rangest::const_iterator ranges_it =
288 for(object_map_dt::vrange_listt::const_iterator r_it =
289 ranges_it->second.begin();
290 r_it!=ranges_it->second.end();
295 if(r_it->function==at_function)
298 flatten_rec(fi->second, temp, seen, r_it->function, r_it->from);
304 if(t_it->second.offset_is_set &&
305 it->second.offset_is_set)
307 t_it->second.offset += it->second.offset;
310 t_it->second.offset_is_set=
false;
328 it->second.offset_is_set=
false;
329 for(std::list<const object_map_dt::vrange_listt*>::const_iterator vit =
331 vit!=add_ranges.end();
334 for(object_map_dt::vrange_listt::const_iterator lit =
343 seen.erase(identifier + e.
suffix);
350 if(
object.
id()==ID_invalid ||
351 object.
id()==ID_unknown)
358 if(it->second.offset_is_set)
402 dest.
write()[it->first]=it->second;
412 std::list<exprt> &value_set,
423 if(
object.type().id()==
"#REF#")
425 assert(
object.
id()==ID_symbol);
427 const irep_idt &ident=
object.get(ID_identifier);
428 valuest::const_iterator v_it=
values.find(ident);
439 if(t_it->second.offset_is_set &&
440 it->second.offset_is_set)
442 t_it->second.offset += it->second.offset;
445 t_it->second.offset_is_set=
false;
447 flat_map.
write()[t_it->first]=t_it->second;
452 flat_map.
write()[it->first]=it->second;
456 value_set.push_back(
to_expr(fit));
460 for(std::list<exprt>::const_iterator it=value_set.begin();
463 assert(it->type().id()!=
"#REF");
467 for(std::list<exprt>::const_iterator it=value_set.begin();
470 std::cout <<
"GET_VALUE_SET: " <<
from_expr(ns,
"", *it) <<
'\n';
489 const std::string &suffix,
490 const typet &original_type,
495 std::cout <<
"GET_VALUE_SET_REC EXPR: " << expr <<
'\n';
496 std::cout <<
"GET_VALUE_SET_REC SUFFIX: " << suffix <<
'\n';
500 if(expr.type().id()==
"#REF#")
502 valuest::const_iterator fi=
values.find(expr.get(ID_identifier));
508 original_type, ns, recursion_set);
517 else if(expr.id()==ID_unknown || expr.id()==ID_invalid)
522 else if(expr.id()==ID_index)
524 assert(expr.operands().size()==2);
528 assert(type.id()==ID_array ||
529 type.id()==ID_incomplete_array ||
533 original_type, ns, recursion_set);
537 else if(expr.id()==ID_member)
539 assert(expr.operands().size()==1);
541 if(expr.op0().is_not_nil())
545 assert(type.
id()==ID_struct ||
546 type.
id()==ID_union ||
547 type.
id()==ID_incomplete_struct ||
548 type.
id()==ID_incomplete_union);
550 const std::string &component_name=
554 original_type, ns, recursion_set);
559 else if(expr.id()==ID_symbol)
563 irep_idt ident=expr.get_string(ID_identifier)+suffix;
572 valuest::const_iterator v_it=
values.find(ident);
584 else if(expr.id()==ID_if)
586 if(expr.operands().size()!=3)
587 throw "if takes three operands";
590 original_type, ns, recursion_set);
592 original_type, ns, recursion_set);
596 else if(expr.id()==ID_address_of)
598 if(expr.operands().size()!=1)
599 throw expr.id_string()+
" expected to have one operand";
605 else if(expr.id()==ID_dereference)
611 if(object_map.
begin()!=object_map.
end())
617 original_type, ns, recursion_set);
623 else if(expr.id()==
"reference_to")
631 if(object_map.
begin()!=object_map.
end())
637 original_type, ns, recursion_set);
643 else if(expr.is_constant())
646 if(expr.get(ID_value)==ID_NULL &&
647 expr.type().id()==ID_pointer)
653 else if(expr.id()==ID_typecast)
655 if(expr.operands().size()!=1)
656 throw "typecast takes one operand";
659 original_type, ns, recursion_set);
663 else if(expr.id()==ID_plus || expr.id()==ID_minus)
665 if(expr.operands().size()<2)
666 throw expr.id_string()+
" expected to have at least two operands";
668 if(expr.type().id()==ID_pointer)
671 const exprt *ptr_operand=
nullptr;
674 if(it->type().id()==ID_pointer)
676 if(ptr_operand==
nullptr)
679 throw "more than one pointer operand in pointer arithmetic";
682 if(ptr_operand==
nullptr)
683 throw "pointer type sum expected to have pointer operand";
687 ptr_operand->
type(), ns, recursion_set);
693 if(
object.offset_is_zero() &&
694 expr.operands().size()==2)
696 if(expr.op0().type().id()!=ID_pointer)
702 object.offset=(expr.id()==ID_plus)? i : -i;
708 object.offset_is_set=
false;
710 object.offset=(expr.id()==ID_plus)? i : -i;
714 object.offset_is_set=
false;
722 else if(expr.id()==ID_side_effect)
724 const irep_idt &statement=expr.get(ID_statement);
726 if(statement==ID_function_call)
729 throw "unexpected function_call sideeffect";
731 else if(statement==ID_malloc)
733 if(expr.type().id()!=ID_pointer)
734 throw "malloc expected to return pointer type";
738 const typet &dynamic_type=
739 static_cast<const typet &
>(expr.find(ID_C_cxx_alloc_type));
750 else if(statement==ID_cpp_new ||
751 statement==ID_cpp_new_array)
754 assert(expr.type().id()==ID_pointer);
766 else if(expr.id()==ID_struct)
772 else if(expr.id()==ID_with ||
773 expr.id()==ID_array_of ||
777 throw "unexpected value in get_value_set: "+expr.id_string();
779 else if(expr.id()==ID_dynamic_object)
784 const std::string name=
785 "value_set::dynamic_object"+
790 valuest::const_iterator v_it=
values.find(name);
807 if(src.
id()==ID_typecast)
809 assert(src.
type().
id()==ID_pointer);
812 throw "typecast expects one operand";
832 if(expr.
type().
id()==
"#REF#")
835 valuest::const_iterator vit=
values.find(ident);
840 dest.insert(
exprt(ID_unknown, expr.
type()));
851 if(t_it->second.offset_is_set &&
852 it->second.offset_is_set)
854 t_it->second.offset += it->second.offset;
857 t_it->second.offset_is_set=
false;
887 std::cout <<
"GET_REFERENCE_SET_REC EXPR: " <<
from_expr(ns,
"", expr)
891 if(expr.
type().
id()==
"#REF#")
893 valuest::const_iterator fi=
values.find(expr.
get(ID_identifier));
901 else if(expr.
id()==ID_symbol ||
902 expr.
id()==ID_dynamic_object ||
903 expr.
id()==ID_string_constant)
905 if(expr.
type().
id()==ID_array &&
913 else if(expr.
id()==ID_dereference)
916 throw expr.
id_string()+
" expected to have one operand";
926 if(obj.
type().
id()==
"#REF#")
929 valuest::const_iterator v_it=
values.find(ident);
940 if(t_it->second.offset_is_set &&
941 it->second.offset_is_set)
943 t_it->second.offset += it->second.offset;
946 t_it->second.offset_is_set=
false;
960 for(expr_sett::const_iterator it=value_set.begin();
963 std::cout <<
"VALUE_SET: " <<
from_expr(ns,
"", *it) <<
'\n';
968 else if(expr.
id()==ID_index)
971 throw "index expected to have two operands";
977 assert(array_type.
id()==ID_array ||
978 array_type.
id()==ID_incomplete_array);
989 if(
object.
id()==ID_unknown)
995 index_expr.op0()=object;
999 if(
object.type().
id()!=
"#REF#" &&
1000 ns.
follow(
object.type())!=array_type)
1001 index_expr.make_typecast(array.
type());
1021 else if(expr.
id()==ID_member)
1023 const irep_idt &component_name=expr.
get(ID_component_name);
1026 throw "member expected to have one operand";
1040 if(
object.
id()==ID_unknown)
1042 else if(
object.
id()==ID_dynamic_object &&
1043 obj_type.
id()!=ID_struct &&
1044 obj_type.
id()!=ID_union)
1054 exprt member_expr(ID_member, expr.
type());
1056 member_expr.set(ID_component_name, component_name);
1060 member_expr.op0().make_typecast(struct_op.
type());
1068 else if(expr.
id()==ID_if)
1071 throw "if takes three operands";
1088 std::cout <<
"ASSIGN LHS: " << lhs <<
'\n';
1089 std::cout <<
"ASSIGN LTYPE: " << ns.
follow(lhs.type()) <<
'\n';
1090 std::cout <<
"ASSIGN RHS: " <<
from_expr(ns,
"", rhs) <<
'\n';
1096 throw "if takes three operands";
1098 assign(lhs, rhs.
op1(), ns, add_to_sets);
1105 if(type.
id()==ID_struct ||
1106 type.
id()==ID_union)
1112 for(struct_typet::componentst::const_iterator
1117 const typet &subtype=c_it->type();
1118 const irep_idt &name=c_it->get(ID_name);
1121 if(subtype.
id()==ID_code)
1124 exprt lhs_member(ID_member, subtype);
1125 lhs_member.
set(ID_component_name, name);
1130 if(rhs.
id()==ID_unknown ||
1131 rhs.
id()==ID_invalid)
1133 rhs_member=
exprt(rhs.
id(), subtype);
1139 "type mismatch:\nRHS: "+rhs.
type().
pretty()+
"\n"+
1142 if(rhs.
id()==ID_struct ||
1143 rhs.
id()==ID_constant)
1148 else if(rhs.
id()==ID_with)
1153 const exprt &member_operand=rhs.
op1();
1156 member_operand.get(ID_component_name);
1158 if(component_name==name)
1161 rhs_member=rhs.
op2();
1166 rhs_member=
exprt(ID_member, subtype);
1168 rhs_member.
set(ID_component_name, name);
1173 rhs_member=
exprt(ID_member, subtype);
1175 rhs_member.
set(ID_component_name, name);
1178 assign(lhs_member, rhs_member, ns, add_to_sets);
1182 else if(type.
id()==ID_array)
1187 if(rhs.
id()==ID_unknown ||
1188 rhs.
id()==ID_invalid)
1196 if(rhs.
id()==ID_array_of)
1200 assign(lhs_index, rhs.
op0(), ns, add_to_sets);
1202 else if(rhs.
id()==ID_array ||
1203 rhs.
id()==ID_constant)
1207 assign(lhs_index, *o_it, ns, add_to_sets);
1210 else if(rhs.
id()==ID_with)
1217 assign(lhs_index, op0_index, ns, add_to_sets);
1224 assign(lhs_index, rhs_index, ns,
true);
1236 assign_rec(lhs, values_rhs,
"", ns, recset, add_to_sets);
1245 if(op.
type().
id()!=ID_pointer)
1246 throw "free expected to have pointer-type operand";
1264 if(
object.
id()==ID_dynamic_object)
1276 for(valuest::iterator v_it=
values.begin();
1283 v_it->second.object_map.read();
1291 if(
object.
id()==ID_dynamic_object)
1297 set(new_object_map, o_it);
1309 set(new_object_map, o_it);
1315 v_it->second.suffix);
1324 const std::string &suffix,
1330 std::cout <<
"ASSIGN_REC LHS: " << lhs <<
'\n';
1331 std::cout <<
"ASSIGN_REC SUFFIX: " << suffix <<
'\n';
1334 it!=values_rhs.
read().
end(); it++)
1335 std::cout <<
"ASSIGN_REC RHS: " <<
to_expr(it) <<
'\n';
1338 if(lhs.type().id()==
"#REF#")
1340 const irep_idt &ident=lhs.get(ID_identifier);
1345 if(recursion_set.find(ident)!=recursion_set.end())
1347 recursion_set.insert(ident);
1351 suffix, ns, recursion_set, add_to_sets);
1353 recursion_set.erase(ident);
1356 else if(lhs.id()==ID_symbol)
1358 const irep_idt &identifier=lhs.get(ID_identifier);
1361 "value_set::dynamic_object") ||
1363 "value_set::return_value") ||
1383 else if(lhs.id()==ID_dynamic_object)
1388 const std::string name=
1389 "value_set::dynamic_object"+
1405 make_union(temp_entry.object_map, values_rhs);
1407 else if(lhs.id()==ID_dereference)
1409 if(lhs.operands().size()!=1)
1410 throw lhs.id_string()+
" expected to have one operand";
1419 if(
object.
id()!=ID_unknown)
1420 assign_rec(
object, values_rhs, suffix, ns, recursion_set, add_to_sets);
1423 else if(lhs.id()==ID_index)
1425 if(lhs.operands().size()!=2)
1426 throw "index expected to have two operands";
1430 assert(type.
id()==ID_array ||
1431 type.
id()==ID_incomplete_array ||
1432 type.
id()==
"#REF#");
1435 lhs.op0(), values_rhs,
"[]"+suffix, ns, recursion_set, add_to_sets);
1437 else if(lhs.id()==ID_member)
1439 if(lhs.operands().size()!=1)
1440 throw "member expected to have one operand";
1442 if(lhs.op0().is_nil())
1445 const std::string &component_name=lhs.get_string(ID_component_name);
1449 assert(type.
id()==ID_struct ||
1450 type.
id()==ID_union ||
1451 type.
id()==ID_incomplete_struct ||
1452 type.
id()==ID_incomplete_union);
1454 assign_rec(lhs.op0(), values_rhs,
"."+component_name+suffix,
1455 ns, recursion_set, add_to_sets);
1457 else if(lhs.id()==
"valid_object" ||
1458 lhs.id()==
"dynamic_size" ||
1459 lhs.id()==
"dynamic_type")
1463 else if(lhs.id()==ID_string_constant)
1468 else if(lhs.id()==
"NULL-object")
1472 else if(lhs.id()==ID_typecast)
1477 ns, recursion_set, add_to_sets);
1479 else if(lhs.id()==
"zero_string" ||
1480 lhs.id()==
"is_zero_string" ||
1481 lhs.id()==
"zero_string_length")
1485 else if(lhs.id()==ID_byte_extract_little_endian ||
1486 lhs.id()==ID_byte_extract_big_endian)
1488 assert(lhs.operands().size()==2);
1489 assign_rec(lhs.op0(), values_rhs, suffix, ns, recursion_set,
true);
1492 throw "assign NYI: `"+lhs.id_string()+
"'";
1517 for(
unsigned i=0; i<arguments.size(); i++)
1519 const std::string identifier=
"value_set::" +
id2string(
function) +
"::" +
1520 "argument$"+std::to_string(i);
1525 assign(dummy_lhs, arguments[i], ns,
true);
1541 for(code_typet::parameterst::const_iterator
1542 it=parameter_types.begin();
1543 it!=parameter_types.end();
1546 const irep_idt &identifier=it->get_identifier();
1554 "argument$"+std::to_string(i), it->type());
1557 assign(actual_lhs, v_expr, ns,
true);
1569 std::string rvs=
"value_set::return_value" + std::to_string(
from_function);
1581 if(statement==ID_block)
1586 else if(statement==ID_function_call)
1591 else if(statement==ID_assign ||
1595 throw "assignment expected to have two operands";
1599 else if(statement==ID_decl)
1602 throw "decl expected to have one operand";
1606 if(lhs.
id()!=ID_symbol)
1607 throw "decl expected to have symbol on lhs";
1611 else if(statement==ID_specc_notify ||
1612 statement==ID_specc_wait)
1616 else if(statement==ID_expression)
1620 else if(statement==ID_cpp_delete ||
1621 statement==ID_cpp_delete_array)
1625 else if(statement==ID_free)
1630 throw "free expected to have one operand";
1634 else if(statement==
"lock" || statement==
"unlock")
1638 else if(statement==ID_asm)
1642 else if(statement==ID_nondet)
1646 else if(statement==ID_printf)
1650 else if(statement==ID_return)
1655 std::string rvs=
"value_set::return_value" + std::to_string(
from_function);
1660 else if(statement==ID_input || statement==ID_output)
1668 "value_set_fivrt: unexpected statement: "+
id2string(statement);
1694 if(old.
offset==
object.offset)
1735 if(old.
offset==
object.offset)
1759 for(
unsigned i=vr.
from; i<=vr.
to; i++)
1771 if(is_valid_at(inx, f, line))
1775 vrange_listt::iterator it=ranges.begin();
1777 while(it->function!=f && it!=ranges.end()) it++;
1780 it!=ranges.end() && it->function==f && it->from <= line;
1785 if( line == it->to+1)
1790 vrange_listt::iterator n_it=it; n_it++;
1791 if(n_it!=ranges.end() &&
1792 it->function == n_it->function &&
1793 it->to+1 == n_it->from)
1795 n_it->from=it->from;
1796 it=ranges.erase(it);
1806 if(it!=ranges.end())
1810 if( line == it->from - 1)
1815 if(it!=ranges.begin())
1817 vrange_listt::iterator p_it=it; p_it--;
1818 if(p_it->function == it->function &&
1819 p_it->to+1 == it->from)
1822 it=ranges.erase(it);
1832 ranges.insert(it, insr);
1840 unsigned line)
const 1843 std::cout <<
"IS_VALID_AT: " << inx <<
", " << f <<
", line " << line <<
1847 validity_rangest::const_iterator vrs=validity_ranges.find(inx);
1848 if(vrs!=validity_ranges.end())
1852 object_map_dt::vrange_listt::const_iterator it=ranges.begin();
1854 while(it->function!=f &&
1859 it!=ranges.end() && it->function==f && it->from<=line;
1861 if(it->contains(f, line))
1876 if(o.
id()==ID_symbol && o.
get(ID_identifier)==ident)
1878 else if(o.
type().
id()==
"#REF#")
1882 if(recursion_set.find(oid)!=recursion_set.end())
1889 valuest::const_iterator vit=
values.find(oid);
1892 const entryt &e=vit->second;
1894 recursion_set.insert(oid);
1897 recursion_set.erase(oid);
1910 for(valuest::iterator it=
values.begin();
1933 if(
make_union(state_map, t_it->second.object_map))
The type of an expression.
irep_idt name
The unique identifier.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
const typet & follow(const typet &src) const
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
void get_reference_set(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
const std::string & id2string(const irep_idt &d)
const std::string integer2string(const mp_integer &n, unsigned base)
void dereference_rec(const exprt &src, exprt &dest) const
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast a generic exprt to a dynamic_object_exprt.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
#define forall_objects(it, map)
void do_end_function(const exprt &lhs, const namespacet &ns)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
void copy_to_operands(const exprt &expr)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::vector< parametert > parameterst
bool recursive_find(const irep_idt &ident, const object_mapt &rhs, recfind_recursion_sett &recursion_set) const
const componentst & components() const
#define Forall_objects(it, map)
bool make_union(object_mapt &dest, const object_mapt &src) const
objmapt::iterator iterator
void copy_objects(object_mapt &dest, const object_mapt &src) const
void output(const namespacet &ns, std::ostream &out) const
std::unordered_set< exprt, irep_hash > expr_sett
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
bool offset_is_zero() const
unsigned from_target_index
#define Forall_valid_objects(it, map)
void get_reference_set_sharing_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
const irep_idt & id() const
The boolean constant true.
void get_value_set_rec(const exprt &expr, object_mapt &dest, const std::string &suffix, const typet &original_type, const namespacet &ns, gvs_recursion_sett &recursion_set) const
bool insert_from(object_mapt &dest, object_map_dt::const_iterator it) const
bool is_valid_at(unsigned inx, unsigned f, unsigned line) const
void flatten_rec(const entryt &, object_mapt &, flatten_seent &, unsigned from_function, unsigned from_index) const
API to expression classes.
const irep_idt & get(const irep_namet &name) const
void apply_code(const exprt &code, const namespacet &ns)
std::list< validity_ranget > vrange_listt
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
split an expression into a base object and a (byte) offset
void get_reference_set_sharing(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
#define forall_operands(it, expr)
std::unordered_set< idt, string_hash > gvs_recursion_sett
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns, bool add_to_sets=false)
void get_value_set(const exprt &expr, std::list< exprt > &expr_set, const namespacet &ns) const
bitvector_typet index_type()
bool make_valid_union(object_mapt &dest, const object_mapt &src) const
entryt & get_entry(const idt &id, const std::string &suffix)
static object_numberingt object_numbering
Operator to return the address of an object.
void flatten(const entryt &e, object_mapt &dest) const
static const object_map_dt blank
std::unordered_set< unsigned int > dynamic_object_id_sett
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
entryt & get_temporary_entry(const idt &id, const std::string &suffix)
std::vector< exprt > operandst
bool has_prefix(const std::string &s, const std::string &prefix)
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
bool set_valid_at(unsigned inx, unsigned f, unsigned line)
const irep_idt & display_name() const
static const char * alloc_adapter_prefix
validity_rangest validity_ranges
typet type
Type of symbol.
exprt to_expr(object_map_dt::const_iterator it) const
objmapt::const_iterator const_iterator
void assign_rec(const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, assign_recursion_sett &recursion_set, bool add_to_sets)
bool insert_to(object_mapt &dest, object_map_dt::const_iterator it) const
Base class for all expressions.
const parameterst & parameters() const
#define forall_valid_objects(it, map)
Value Set (Flow Insensitive, Sharing, Validity Regions)
static hash_numbering< irep_idt, irep_id_hash > function_numbering
std::unordered_set< idt, string_hash > flatten_seent
const std::string & get_string(const irep_namet &name) const
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
const std::string & id_string() const
void add_var(const idt &id, const std::string &suffix)
Expression to hold a symbol (variable)
exprt dynamic_object(const exprt &pointer)
std::unordered_set< idt, string_hash > assign_recursion_sett
const typet & subtype() const
void do_free(const exprt &op, const namespacet &ns)
std::unordered_set< idt, string_hash > recfind_recursion_sett
void set(const irep_namet &name, const irep_idt &value)
const_iterator find(unsigned k)
bool simplify(exprt &expr, const namespacet &ns)