@@ -97,21 +97,21 @@ exprt value_set_dereferencet::dereference(const exprt &pointer)
9797 // type of the object
9898 const typet &type=pointer.type ().subtype ();
9999
100- #if 0
101- std::cout << "DEREF: " << format(pointer) << '\n';
100+ #ifdef DEBUG
101+ std::cout << " value_set_dereferencet::dereference pointer=" << format (pointer)
102+ << ' \n ' ;
102103#endif
103104
104105 // collect objects the pointer may point to
105106 value_setst::valuest points_to_set;
106107
107108 dereference_callback.get_value_set (pointer, points_to_set);
108109
109- #if 0
110- for(value_setst::valuest::const_iterator
111- it=points_to_set.begin();
112- it!=points_to_set.end();
113- it++)
114- std::cout << "P: " << format(*it) << '\n';
110+ #ifdef DEBUG
111+ std::cout << " value_set_dereferencet::dereference points_to_set={" ;
112+ for (auto p : points_to_set)
113+ std::cout << format (p) << " ; " ;
114+ std::cout << " }\n " << std::flush;
115115#endif
116116
117117 // get the values of these
@@ -140,15 +140,15 @@ exprt value_set_dereferencet::dereference(const exprt &pointer)
140140 compare_against_pointer = fresh_binder.symbol_expr ();
141141 }
142142
143+ #ifdef DEBUG
144+ std::cout << " value_set_dereferencet::dereference retained_values={" ;
143145 for (const auto &value : retained_values)
144- {
145- values.push_back (build_reference_to (value, compare_against_pointer, ns));
146- #if 0
147- std::cout << "V: " << format(value.pointer_guard) << " --> ";
148- std::cout << format(value.value);
149- std::cout << '\n';
146+ std::cout << format (value) << " ; " ;
147+ std::cout << " }\n " << std::flush;
150148#endif
151- }
149+
150+ for (const auto &value : retained_values)
151+ values.push_back (build_reference_to (value, compare_against_pointer, ns));
152152
153153 // can this fail?
154154 bool may_fail;
@@ -227,8 +227,10 @@ exprt value_set_dereferencet::dereference(const exprt &pointer)
227227 if (compare_against_pointer != pointer)
228228 value = let_exprt (to_symbol_expr (compare_against_pointer), pointer, value);
229229
230- #if 0
231- std::cout << "R: " << format(value) << "\n\n";
230+ #ifdef DEBUG
231+ std::cout << " value_set_derefencet::dereference value=" << format (value)
232+ << ' \n '
233+ << std::flush;
232234#endif
233235
234236 return value;
0 commit comments