Skip to content

Commit

Permalink
namespacet::follow: also follow enum tags
Browse files Browse the repository at this point in the history
`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.
  • Loading branch information
tautschnig committed Feb 13, 2024
1 parent 9c7bccc commit 4ac7136
Show file tree
Hide file tree
Showing 2 changed files with 17 additions and 0 deletions.
14 changes: 14 additions & 0 deletions regression/goto-instrument/nondet-volatile-01/test.c
Original file line number Diff line number Diff line change
@@ -1,5 +1,15 @@
#include <assert.h>

enum E
{
A,
B
};

int main()
{
}

void main()
{
int a[2] = {0};
Expand All @@ -8,4 +18,8 @@ void main()
a[i] = 1;

assert(a[1] == 0); // should fail

// make sure the use of enum (tags) does not cause infinite recursion
enum A a = A;
a = a;
}
3 changes: 3 additions & 0 deletions src/util/namespace.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,9 @@ const typet &namespace_baset::follow(const typet &src) const
if(src.id() == ID_struct_tag)
return follow_tag(to_struct_tag_type(src));

if(src.id() == ID_c_enum_tag)
return follow_tag(to_c_enum_tag_type(src));

return src;
}

Expand Down

0 comments on commit 4ac7136

Please sign in to comment.