Skip to content

Commit 0e3e26f

Browse files
committed
namespacet::follow: also follow enum tags
`follow` is a catch-all for tagged (and untagged) types that should do all variants of `follow_tag`. Fixes an unbounded recursion when using nondet-volatile on programs that use enums.
1 parent 1590a31 commit 0e3e26f

File tree

2 files changed

+13
-0
lines changed

2 files changed

+13
-0
lines changed

regression/goto-instrument/nondet-volatile-01/test.c

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,11 @@
11
#include <assert.h>
22

3+
enum E
4+
{
5+
A,
6+
B
7+
};
8+
39
void main()
410
{
511
int a[2] = {0};
@@ -8,4 +14,8 @@ void main()
814
a[i] = 1;
915

1016
assert(a[1] == 0); // should fail
17+
18+
// make sure the use of enum (tags) does not cause infinite recursion
19+
enum A e = A;
20+
e = e;
1121
}

src/util/namespace.cpp

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -54,6 +54,9 @@ const typet &namespace_baset::follow(const typet &src) const
5454
if(src.id() == ID_struct_tag)
5555
return follow_tag(to_struct_tag_type(src));
5656

57+
if(src.id() == ID_c_enum_tag)
58+
return follow_tag(to_c_enum_tag_type(src));
59+
5760
return src;
5861
}
5962

0 commit comments

Comments
 (0)