Skip to content

Commit b5fa7b7

Browse files
committed
requires_renaming must not recurse into array subtypes in structs
Just like pointers, array members may have subtypes of the same type as the containing struct. The behaviour/check now matches what the actual renaming function uses. Also clean up the unnecessary ID_class, which does not actually exist.
1 parent f4dedec commit b5fa7b7

File tree

3 files changed

+27
-3
lines changed

3 files changed

+27
-3
lines changed

regression/cbmc/struct12/main.c

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
struct S
2+
{
3+
struct S *s;
4+
struct S *a[2];
5+
};
6+
7+
int main()
8+
{
9+
struct S s;
10+
s.s = 0;
11+
return 0;
12+
}

regression/cbmc/struct12/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

src/goto-symex/goto_symex_state.cpp

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -622,16 +622,20 @@ static bool requires_renaming(const typet &type, const namespacet &ns)
622622
return requires_renaming(array_type.subtype(), ns) ||
623623
!array_type.size().is_constant();
624624
}
625-
else if(
626-
type.id() == ID_struct || type.id() == ID_union || type.id() == ID_class)
625+
else if(type.id() == ID_struct || type.id() == ID_union)
627626
{
628627
const struct_union_typet &s_u_type = to_struct_union_type(type);
629628
const struct_union_typet::componentst &components = s_u_type.components();
630629

631630
for(auto &component : components)
632631
{
633632
// be careful, or it might get cyclic
634-
if(
633+
if(component.type().id() == ID_array)
634+
{
635+
if(!to_array_type(component.type()).size().is_constant())
636+
return true;
637+
}
638+
else if(
635639
component.type().id() != ID_pointer &&
636640
requires_renaming(component.type(), ns))
637641
{

0 commit comments

Comments
 (0)