Skip to content

Commit c159fa2

Browse files
author
Lukasz A.J. Wrona
committed
Make message::get_mstream const
Changes message::mstream object to mutable so that message::debug() and its friends can be run by constant methods. Warning: in the future, when implementing multiple threads, implementation of get_mstream will have to be changed so that each thread has its own, local standard output. As it stands each get_mstream() call changes stream type for the whole program.
1 parent 0cd1057 commit c159fa2

File tree

1 file changed

+9
-9
lines changed

1 file changed

+9
-9
lines changed

src/util/message.h

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -236,50 +236,50 @@ class messaget
236236
return m;
237237
}
238238

239-
mstreamt &get_mstream(unsigned message_level)
239+
mstreamt &get_mstream(unsigned message_level) const
240240
{
241241
mstream.message_level=message_level;
242242
return mstream;
243243
}
244244

245-
mstreamt &error()
245+
mstreamt &error() const
246246
{
247247
return get_mstream(M_ERROR);
248248
}
249249

250-
mstreamt &warning()
250+
mstreamt &warning() const
251251
{
252252
return get_mstream(M_WARNING);
253253
}
254254

255-
mstreamt &result()
255+
mstreamt &result() const
256256
{
257257
return get_mstream(M_RESULT);
258258
}
259259

260-
mstreamt &status()
260+
mstreamt &status() const
261261
{
262262
return get_mstream(M_STATUS);
263263
}
264264

265-
mstreamt &statistics()
265+
mstreamt &statistics() const
266266
{
267267
return get_mstream(M_STATISTICS);
268268
}
269269

270-
mstreamt &progress()
270+
mstreamt &progress() const
271271
{
272272
return get_mstream(M_PROGRESS);
273273
}
274274

275-
mstreamt &debug()
275+
mstreamt &debug() const
276276
{
277277
return get_mstream(M_DEBUG);
278278
}
279279

280280
protected:
281281
message_handlert *message_handler;
282-
mstreamt mstream;
282+
mutable mstreamt mstream;
283283
};
284284

285285
#endif // CPROVER_UTIL_MESSAGE_H

0 commit comments

Comments
 (0)