diff --git a/regression/goto-instrument/nondet-volatile-01/test.c b/regression/goto-instrument/nondet-volatile-01/test.c index ec0cc273a79..7dee1ec9cff 100644 --- a/regression/goto-instrument/nondet-volatile-01/test.c +++ b/regression/goto-instrument/nondet-volatile-01/test.c @@ -1,5 +1,11 @@ #include +enum E +{ + A, + B +}; + void main() { int a[2] = {0}; @@ -8,4 +14,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 e = A; + e = e; } diff --git a/src/goto-instrument/nondet_volatile.cpp b/src/goto-instrument/nondet_volatile.cpp index 5423c25b61e..a145c106496 100644 --- a/src/goto-instrument/nondet_volatile.cpp +++ b/src/goto-instrument/nondet_volatile.cpp @@ -13,6 +13,7 @@ Date: September 2011 #include "nondet_volatile.h" +#include #include #include #include @@ -94,14 +95,14 @@ bool nondet_volatilet::is_volatile(const namespacet &ns, const typet &src) if(src.get_bool(ID_C_volatile)) return true; - if( - src.id() == ID_struct_tag || src.id() == ID_union_tag || - src.id() == ID_c_enum_tag) - { - return is_volatile(ns, ns.follow(src)); - } - - return false; + if(auto struct_tag = type_try_dynamic_cast(src)) + return is_volatile(ns, ns.follow_tag(*struct_tag)); + else if(auto union_tag = type_try_dynamic_cast(src)) + return is_volatile(ns, ns.follow_tag(*union_tag)); + else if(auto enum_tag = type_try_dynamic_cast(src)) + return is_volatile(ns, ns.follow_tag(*enum_tag)); + else + return false; } void nondet_volatilet::handle_volatile_expression(