File tree Expand file tree Collapse file tree 1 file changed +5
-4
lines changed
Expand file tree Collapse file tree 1 file changed +5
-4
lines changed Original file line number Diff line number Diff line change @@ -29,6 +29,7 @@ Author: Daniel Kroening, kroening@kroening.com
2929#include < util/options.h>
3030#include < util/pointer_offset_size.h>
3131#include < util/pointer_predicates.h>
32+ #include < util/range.h>
3233#include < util/simplify_expr.h>
3334#include < util/ssa_expr.h>
3435
@@ -123,8 +124,6 @@ exprt value_set_dereferencet::dereference(const exprt &pointer)
123124 retained_values.push_back (value);
124125 }
125126
126- std::list<valuet> values;
127-
128127 exprt compare_against_pointer = pointer;
129128
130129 if (retained_values.size () >= 2 && should_use_local_definition_for (pointer))
@@ -147,8 +146,10 @@ exprt value_set_dereferencet::dereference(const exprt &pointer)
147146 std::cout << " }\n " << std::flush;
148147#endif
149148
150- for (const auto &value : retained_values)
151- values.push_back (build_reference_to (value, compare_against_pointer, ns));
149+ std::list<valuet> values =
150+ make_range (retained_values).map ([&](const exprt &value) {
151+ return build_reference_to (value, compare_against_pointer, ns);
152+ });
152153
153154 // can this fail?
154155 bool may_fail;
You can’t perform that action at this time.
0 commit comments