Skip to content

Commit b419e36

Browse files
Improve debug logging of value_set_dereferencet
Use #ifdef DEBUG instead of #if 0 so that compilation of the code can be tested on CI, and make the messages more explecit so that their origin can be recovered when seen in the logs.
1 parent 7734b53 commit b419e36

File tree

1 file changed

+18
-17
lines changed

1 file changed

+18
-17
lines changed

src/pointer-analysis/value_set_dereference.cpp

+18-17
Original file line numberDiff line numberDiff line change
@@ -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 << '}' << std::endl;
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 << '}' << std::endl;
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,9 @@ 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+
<< std::endl;
232233
#endif
233234

234235
return value;

0 commit comments

Comments
 (0)