@@ -142,22 +142,10 @@ exprt value_set_dereferencet::dereference(
142142 // type of the object
143143 const typet &type=pointer.type ().subtype ();
144144
145- #ifdef DEBUG
146- std::cout << " value_set_dereferencet::dereference pointer=" << format (pointer)
147- << ' \n ' ;
148- #endif
149-
150145 // collect objects the pointer may point to
151146 const std::vector<exprt> points_to_set =
152147 dereference_callback.get_value_set (pointer);
153148
154- #ifdef DEBUG
155- std::cout << " value_set_dereferencet::dereference points_to_set={" ;
156- for (auto p : points_to_set)
157- std::cout << format (p) << " ; " ;
158- std::cout << " }\n " << std::flush;
159- #endif
160-
161149 // get the values of these
162150 const std::vector<exprt> retained_values =
163151 make_range (points_to_set).filter ([&](const exprt &value) {
@@ -179,13 +167,6 @@ exprt value_set_dereferencet::dereference(
179167 compare_against_pointer = fresh_binder.symbol_expr ();
180168 }
181169
182- #ifdef DEBUG
183- std::cout << " value_set_dereferencet::dereference retained_values={" ;
184- for (const auto &value : retained_values)
185- std::cout << format (value) << " ; " ;
186- std::cout << " }\n " << std::flush;
187- #endif
188-
189170 std::list<valuet> values =
190171 make_range (retained_values).map ([&](const exprt &value) {
191172 return build_reference_to (value, compare_against_pointer, ns);
@@ -268,17 +249,12 @@ exprt value_set_dereferencet::dereference(
268249 if (compare_against_pointer != pointer)
269250 value = let_exprt (to_symbol_expr (compare_against_pointer), pointer, value);
270251
271- #ifdef DEBUG
272- std::cout << " value_set_derefencet::dereference value=" << format (value)
273- << ' \n '
274- << std::flush;
275- #endif
276-
277252 if (display_points_to_sets)
278253 {
279254 log.status () << value_set_dereference_stats_to_json (
280255 pointer, points_to_set, retained_values, value);
281256 }
257+
282258 return value;
283259}
284260
0 commit comments