@@ -7,6 +7,7 @@ Author: Daniel Kroening, kroening@kroening.com
77\*******************************************************************/
88
99
10+ #include < unordered_set>
1011#include " expr_util.h"
1112
1213#include " expr.h"
@@ -140,28 +141,35 @@ bool has_subtype(
140141 const std::function<bool (const typet &)> &pred,
141142 const namespacet &ns)
142143{
143- if (pred (type))
144- return true ;
145- else if (type.id () == ID_symbol)
146- return has_subtype (ns.follow (type), pred, ns);
147- else if (type.id () == ID_c_enum_tag)
148- return has_subtype (ns.follow_tag (to_c_enum_tag_type (type)), pred, ns);
149- else if (type.id () == ID_struct || type.id () == ID_union)
150- {
151- const struct_union_typet &struct_union_type = to_struct_union_type (type);
144+ std::vector<typet> stack (1 , type);
145+ std::unordered_set<typet, irep_hash> visited;
152146
153- for (const auto &comp : struct_union_type.components ())
154- if (has_subtype (comp.type (), pred, ns))
155- return true ;
156- }
157- // do not look into pointer subtypes as this could cause unbounded recursion
158- else if (type.id () == ID_array || type.id () == ID_vector)
159- return has_subtype (type.subtype (), pred, ns);
160- else if (type.has_subtypes ())
147+ const auto push_if_not_visited = [&](const typet &t) {
148+ if (!visited.insert (t).second )
149+ stack.push_back (t);
150+ };
151+
152+ while (!stack.empty ())
161153 {
162- for (const auto &subtype : type.subtypes ())
163- if (has_subtype (subtype, pred, ns))
164- return true ;
154+ const typet &top= stack.back ();
155+ stack.pop_back ();
156+
157+ if (pred (top))
158+ return true ;
159+ else if (top.id () == ID_symbol)
160+ push_if_not_visited (ns.follow (top));
161+ else if (top.id () == ID_c_enum_tag)
162+ push_if_not_visited (ns.follow_tag (to_c_enum_tag_type (top)));
163+ else if (top.id () == ID_struct || top.id () == ID_union)
164+ {
165+ for (const auto &comp : to_struct_union_type (top).components ())
166+ push_if_not_visited (comp.type ());
167+ }
168+ else if (top.has_subtypes ())
169+ {
170+ for (const auto &subtype : top.subtypes ())
171+ push_if_not_visited (subtype);
172+ }
165173 }
166174
167175 return false ;
0 commit comments