Skip to content

Commit 279cb5f

Browse files
committed
SMT back-end: nested empty structs also have zero width
This extends the check introduced in c3d954e to account for structs comprised of empty structs (as found in the Malloc10 regression test).
1 parent bf18c17 commit 279cb5f

File tree

1 file changed

+9
-4
lines changed

1 file changed

+9
-4
lines changed

src/solvers/smt2/smt2_conv.cpp

Lines changed: 9 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -965,12 +965,17 @@ static bool is_zero_width(const typet &type, const namespacet &ns)
965965
return true;
966966
else if(type.id() == ID_struct_tag)
967967
return is_zero_width(ns.follow_tag(to_struct_tag_type(type)), ns);
968-
else if(type.id() == ID_struct)
969-
return to_struct_type(type).components().empty();
970968
else if(type.id() == ID_union_tag)
971969
return is_zero_width(ns.follow_tag(to_union_tag_type(type)), ns);
972-
else if(type.id() == ID_union)
973-
return to_union_type(type).components().empty();
970+
else if(type.id() == ID_struct || type.id() == ID_union)
971+
{
972+
for(const auto &comp : to_struct_union_type(type).components())
973+
{
974+
if(!is_zero_width(comp.type(), ns))
975+
return false;
976+
}
977+
return true;
978+
}
974979
else
975980
return false;
976981
}

0 commit comments

Comments
 (0)