Skip to content

Commit 2d8ca77

Browse files
committed
Failing test to show that requires_renaming recurses
requires_renaming must not recurse into array subtypes in structs.
1 parent ce3e340 commit 2d8ca77

File tree

2 files changed

+24
-0
lines changed

2 files changed

+24
-0
lines changed

regression/cbmc/struct13/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/struct13/test.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
KNOWNBUG
2+
main.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring
9+
--
10+
Just like pointers, array members may have subtypes of the same type as the
11+
containing struct. requires_renaming fails to catch this case, which results in
12+
unbounded recursion.

0 commit comments

Comments
 (0)