Skip to content

Commit fcdd39b

Browse files
author
Daniel Kroening
committed
tolerate imprecision in value_sett
1 parent 9507b78 commit fcdd39b

File tree

1 file changed

+13
-4
lines changed

1 file changed

+13
-4
lines changed

src/pointer-analysis/value_set.cpp

Lines changed: 13 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1202,9 +1202,14 @@ void value_sett::assign(
12021202
"rhs.type():\n"+rhs.type().pretty()+"\n"+
12031203
"type:\n"+type.pretty();
12041204

1205-
rhs_member=make_member(rhs, name, ns);
1205+
const typet &followed = ns.follow(rhs.type());
12061206

1207-
assign(lhs_member, rhs_member, ns, is_simplified, add_to_sets);
1207+
if(followed.id() == ID_struct || followed.id() == ID_union)
1208+
{
1209+
rhs_member = make_member(rhs, name, ns);
1210+
1211+
assign(lhs_member, rhs_member, ns, is_simplified, add_to_sets);
1212+
}
12081213
}
12091214
}
12101215
}
@@ -1744,15 +1749,19 @@ exprt value_sett::make_member(
17441749
if(component_name==member_operand.get(ID_component_name))
17451750
// yes! just take op2
17461751
return src.op2();
1747-
else
1752+
else if(ns.follow(src.op0().type()).id() == ID_struct)
1753+
{
17481754
// no! do this recursively
17491755
return make_member(src.op0(), component_name, ns);
1756+
}
17501757
}
17511758
else if(src.id()==ID_typecast)
17521759
{
17531760
// push through typecast
17541761
assert(src.operands().size()==1);
1755-
return make_member(src.op0(), component_name, ns);
1762+
const typet &followed = ns.follow(src.op0().type());
1763+
if(followed.id() == ID_struct || followed.id() == ID_union)
1764+
return make_member(src.op0(), component_name, ns);
17561765
}
17571766

17581767
// give up

0 commit comments

Comments
 (0)