Skip to content

Commit 474cb9d

Browse files
Simplify using iterator version of find_symbols
This allows to make more things const and removes a loop, so the code is easier to reason about.
1 parent 85cc566 commit 474cb9d

File tree

1 file changed

+5
-9
lines changed

1 file changed

+5
-9
lines changed

src/goto-symex/postcondition.cpp

Lines changed: 5 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -160,16 +160,12 @@ bool postconditiont::is_used(
160160
else if(expr.id()==ID_dereference)
161161
{
162162
// aliasing may happen here
163-
std::vector<exprt> expr_set =
163+
const std::vector<exprt> expr_set =
164164
value_set.get_value_set(to_dereference_expr(expr).pointer(), ns);
165-
std::unordered_set<irep_idt> symbols;
166-
167-
for(const exprt &e : expr_set)
168-
{
169-
const exprt tmp = get_original_name(e);
170-
find_symbols(tmp, symbols);
171-
}
172-
165+
const auto original_names = make_range(expr_set).map(
166+
[](const exprt &e) { return get_original_name(e); });
167+
const std::unordered_set<irep_idt> symbols =
168+
find_symbols(original_names.begin(), original_names.end());
173169
return symbols.find(identifier)!=symbols.end();
174170
}
175171
else

0 commit comments

Comments
 (0)