File tree Expand file tree Collapse file tree 3 files changed +14
-3
lines changed Expand file tree Collapse file tree 3 files changed +14
-3
lines changed Original file line number Diff line number Diff line change @@ -131,10 +131,8 @@ void concurrency_instrumentationt::instrument(
131
131
132
132
void concurrency_instrumentationt::collect (const exprt &expr)
133
133
{
134
- for (const auto &symbol_expr : find_symbols (expr))
134
+ for (const auto &identifier : find_symbol_identifiers (expr))
135
135
{
136
- const irep_idt &identifier = symbol_expr.get_identifier ();
137
-
138
136
namespacet ns (symbol_table);
139
137
const symbolt &symbol = ns.lookup (identifier);
140
138
Original file line number Diff line number Diff line change @@ -88,6 +88,16 @@ std::set<symbol_exprt> find_symbols(const exprt &src)
88
88
.map ([](const exprt &e) { return to_symbol_expr (e); });
89
89
}
90
90
91
+ std::unordered_set<irep_idt> find_symbol_identifiers (const exprt &src)
92
+ {
93
+ std::unordered_set<irep_idt> result;
94
+ src.visit_pre ([&](const exprt &e) {
95
+ if (e.id () == ID_symbol)
96
+ result.insert (to_symbol_expr (e).get_identifier ());
97
+ });
98
+ return result;
99
+ }
100
+
91
101
void find_symbols (kindt kind, const typet &src, find_symbols_sett &dest);
92
102
93
103
void find_symbols (kindt kind, const exprt &src, find_symbols_sett &dest)
Original file line number Diff line number Diff line change @@ -63,6 +63,9 @@ void find_symbols(
63
63
// / Find sub expressions with id ID_symbol
64
64
std::set<symbol_exprt> find_symbols (const exprt &src);
65
65
66
+ // / Find identifiers of the sub expressions with id ID_symbol
67
+ std::unordered_set<irep_idt> find_symbol_identifiers (const exprt &src);
68
+
66
69
// / \return true if one of the symbols in \p src is present in \p symbols
67
70
bool has_symbol (
68
71
const exprt &src,
You can’t perform that action at this time.
0 commit comments