cprover
Loading...
Searching...
No Matches
message.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9
10#ifndef CPROVER_UTIL_MESSAGE_H
11#define CPROVER_UTIL_MESSAGE_H
12
13#include <functional>
14#include <iosfwd>
15#include <sstream>
16#include <string>
17
18#include "deprecate.h"
19#include "invariant.h"
20#include "source_location.h"
21
22class json_objectt;
23class jsont;
25class xmlt;
26
28{
29public:
31 {
32 }
33
34 virtual void print(unsigned level, const std::string &message)=0;
35
36 virtual void print(unsigned level, const xmlt &xml) = 0;
37
38 virtual void print(unsigned level, const jsont &json) = 0;
39
40 virtual void print(unsigned level, const structured_datat &data);
41
42 virtual void print(
43 unsigned level,
44 const std::string &message,
45 const source_locationt &location);
46
47 virtual void flush(unsigned) = 0;
48
50 {
51 }
52
54 unsigned get_verbosity() const { return verbosity; }
55
56 std::size_t get_message_count(unsigned level) const
57 {
58 if(level>=message_count.size())
59 return 0;
60
61 return message_count[level];
62 }
63
66 virtual std::string command(unsigned) const
67 {
68 return std::string();
69 }
70
71protected:
72 unsigned verbosity;
73 std::vector<std::size_t> message_count;
74};
75
77{
78public:
83
84 void print(unsigned level, const std::string &message) override
85 {
86 message_handlert::print(level, message);
87 }
88
89 void print(unsigned, const xmlt &) override
90 {
91 }
92
93 void print(unsigned, const jsont &) override
94 {
95 }
96
97 void print(
98 unsigned level,
99 const std::string &message,
100 const source_locationt &) override
101 {
102 print(level, message);
103 }
104
105 void flush(unsigned) override
106 {
107 }
108};
109
111{
112public:
113 explicit stream_message_handlert(std::ostream &_out):out(_out)
114 {
115 }
116
117 void print(unsigned level, const std::string &message) override
118 {
119 message_handlert::print(level, message);
120
121 if(verbosity>=level)
122 out << message << '\n';
123 }
124
125 void print(unsigned, const xmlt &) override
126 {
127 }
128
129 void print(unsigned, const jsont &) override
130 {
131 }
132
133 void flush(unsigned) override
134 {
135 out << std::flush;
136 }
137
138protected:
139 std::ostream &out;
140};
141
155{
156public:
157 // Standard message levels:
158 //
159 // 0 none
160 // 1 only errors
161 // 2 + warnings
162 // 4 + results
163 // 6 + status/phase information
164 // 8 + statistical information
165 // 9 + progress information
166 // 10 + debug info
167
173
174 static unsigned eval_verbosity(
175 const std::string &user_input,
177 message_handlert &dest);
178
183
185 {
186 INVARIANT(
187 message_handler!=nullptr,
188 "message handler should be set before calling get_message_handler");
189 return *message_handler;
190 }
191
192 // constructors, destructor
193
194 DEPRECATED(SINCE(2019, 1, 7, "use messaget(message_handler) instead"))
196 message_handler(nullptr),
198 {
199 }
200
201 messaget(const messaget &other):
203 mstream(other.mstream, *this)
204 {
205 }
206
208 {
211 return *this;
212 }
213
219
220 virtual ~messaget();
221
222 // \brief Class that stores an individual 'message' with a verbosity 'level'.
223 class mstreamt:public std::ostringstream
224 {
225 public:
233
234 mstreamt(const mstreamt &other)=delete;
235
242
243 mstreamt &operator=(const mstreamt &other)=delete;
244
248
250 {
251 if(this->tellp() > 0)
252 *this << eom; // force end of previous message
254 {
256 }
257 return *this;
258 }
259
261
263 {
264 if(this->tellp() > 0)
265 *this << eom; // force end of previous message
267 {
269 }
270 return *this;
271 }
272
273 template <class T>
275 {
276 static_cast<std::ostream &>(*this) << x;
277 return *this;
278 }
279
280 private:
281 void assign_from(const mstreamt &other)
282 {
285 // message, the pointer to my enclosing messaget, remains unaltered.
286 }
287
288 friend class messaget;
289 };
290
291 // Feeding 'eom' into the stream triggers the printing of the message
292 // This is implemented as an I/O manipulator (compare to STL's endl).
293 class eomt
294 {
295 };
296
297 static eomt eom;
298
300 {
302 {
305 m.str(),
308 }
309 m.clear(); // clears error bits
310 m.str(std::string()); // clears the string
312 return m;
313 }
314
315 // This is an I/O manipulator (compare to STL's set_precision).
317 {
318 public:
319 explicit commandt(unsigned _command) : command(_command)
320 {
321 }
322
323 unsigned command;
324 };
325
328 {
330 return m << m.message.message_handler->command(c.command);
331 else
332 return m;
333 }
334
336 static commandt command(unsigned c)
337 {
338 return commandt(c);
339 }
340
343 static const commandt reset;
344
346 static const commandt red;
347
349 static const commandt green;
350
352 static const commandt yellow;
353
355 static const commandt blue;
356
358 static const commandt magenta;
359
361 static const commandt cyan;
362
364 static const commandt bright_red;
365
367 static const commandt bright_green;
368
371
373 static const commandt bright_blue;
374
377
379 static const commandt bright_cyan;
380
382 static const commandt bold;
383
385 static const commandt faint;
386
388 static const commandt italic;
389
391 static const commandt underline;
392
393 mstreamt &get_mstream(unsigned message_level) const
394 {
395 mstream.message_level=message_level;
396 return mstream;
397 }
398
400 {
401 return get_mstream(M_ERROR);
402 }
403
405 {
406 return get_mstream(M_WARNING);
407 }
408
410 {
411 return get_mstream(M_RESULT);
412 }
413
415 {
416 return get_mstream(M_STATUS);
417 }
418
420 {
422 }
423
425 {
426 return get_mstream(M_PROGRESS);
427 }
428
430 {
431 return get_mstream(M_DEBUG);
432 }
433
435 mstreamt &mstream,
436 const std::function<void(mstreamt &)> &output_generator) const;
437
438protected:
441};
442
443#endif // CPROVER_UTIL_MESSAGE_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
void clear()
Definition irep.h:452
Definition json.h:27
void set_verbosity(unsigned _verbosity)
Definition message.h:53
virtual void print(unsigned level, const std::string &message)=0
Definition message.cpp:60
virtual void print(unsigned level, const jsont &json)=0
std::size_t get_message_count(unsigned level) const
Definition message.h:56
virtual ~message_handlert()
Definition message.h:49
std::vector< std::size_t > message_count
Definition message.h:73
unsigned get_verbosity() const
Definition message.h:54
virtual std::string command(unsigned) const
Create an ECMA-48 SGR (Select Graphic Rendition) command.
Definition message.h:66
unsigned verbosity
Definition message.h:72
virtual void flush(unsigned)=0
virtual void print(unsigned level, const xmlt &xml)=0
commandt(unsigned _command)
Definition message.h:319
unsigned command
Definition message.h:323
messaget & message
Definition message.h:246
mstreamt & operator=(const mstreamt &other)=delete
unsigned message_level
Definition message.h:245
mstreamt(const mstreamt &other, messaget &_message)
Definition message.h:236
mstreamt & operator<<(const structured_datat &data)
Definition message.h:262
mstreamt(unsigned _message_level, messaget &_message)
Definition message.h:226
mstreamt(const mstreamt &other)=delete
source_locationt source_location
Definition message.h:247
void assign_from(const mstreamt &other)
Definition message.h:281
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
mstreamt & get_mstream(unsigned message_level) const
Definition message.h:393
static const commandt yellow
render text with yellow foreground color
Definition message.h:352
static const commandt bright_magenta
render text with bright magenta foreground color
Definition message.h:376
static unsigned eval_verbosity(const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest.
Definition message.cpp:105
message_handlert * message_handler
Definition message.h:439
static const commandt magenta
render text with magenta foreground color
Definition message.h:358
friend mstreamt & operator<<(mstreamt &m, eomt)
Definition message.h:299
mstreamt & error() const
Definition message.h:399
static const commandt reset
return to default formatting, as defined by the terminal
Definition message.h:343
mstreamt & debug() const
Definition message.h:429
message_handlert & get_message_handler()
Definition message.h:184
mstreamt & statistics() const
Definition message.h:419
static const commandt green
render text with green foreground color
Definition message.h:349
mstreamt & warning() const
Definition message.h:404
static const commandt faint
render text with faint font
Definition message.h:385
mstreamt & progress() const
Definition message.h:424
static const commandt bold
render text with bold font
Definition message.h:382
static const commandt bright_red
render text with bright red foreground color
Definition message.h:364
static const commandt underline
render underlined text
Definition message.h:391
void conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
Generate output to message_stream using output_generator if the configured verbosity is at least as h...
Definition message.cpp:139
static const commandt bright_cyan
render text with bright cyan foreground color
Definition message.h:379
static const commandt bright_yellow
render text with bright yellow foreground color
Definition message.h:370
virtual ~messaget()
Definition message.cpp:74
virtual void set_message_handler(message_handlert &_message_handler)
Definition message.h:179
messaget(const messaget &other)
Definition message.h:201
message_levelt
Definition message.h:169
@ M_DEBUG
Definition message.h:171
@ M_RESULT
Definition message.h:170
@ M_STATISTICS
Definition message.h:171
@ M_STATUS
Definition message.h:170
@ M_ERROR
Definition message.h:170
@ M_WARNING
Definition message.h:170
@ M_PROGRESS
Definition message.h:171
static const commandt bright_blue
render text with bright blue foreground color
Definition message.h:373
messaget & operator=(const messaget &other)
Definition message.h:207
mstreamt & result() const
Definition message.h:409
static const commandt italic
render italic text
Definition message.h:388
static const commandt red
render text with red foreground color
Definition message.h:346
messaget(message_handlert &_message_handler)
Definition message.h:214
mstreamt mstream
Definition message.h:440
static commandt command(unsigned c)
Create an ECMA-48 SGR (Select Graphic Rendition) command.
Definition message.h:336
static eomt eom
Definition message.h:297
mstreamt & status() const
Definition message.h:414
friend mstreamt & operator<<(mstreamt &m, const commandt &c)
feed a command into an mstreamt
Definition message.h:327
static const commandt cyan
render text with cyan foreground color
Definition message.h:361
static const commandt bright_green
render text with bright green foreground color
Definition message.h:367
static const commandt blue
render text with blue foreground color
Definition message.h:355
void print(unsigned level, const std::string &message) override
Definition message.h:84
void print(unsigned, const jsont &) override
Definition message.h:93
void print(unsigned level, const std::string &message, const source_locationt &) override
Definition message.h:97
void print(unsigned, const xmlt &) override
Definition message.h:89
void flush(unsigned) override
Definition message.h:105
void print(unsigned, const xmlt &) override
Definition message.h:125
void print(unsigned level, const std::string &message) override
Definition message.h:117
stream_message_handlert(std::ostream &_out)
Definition message.h:113
std::ostream & out
Definition message.h:139
void print(unsigned, const jsont &) override
Definition message.h:129
void flush(unsigned) override
Definition message.h:133
A way of representing nested key/value data.
Definition xml.h:21
#define SINCE(year, month, day, msg)
Definition deprecate.h:26
#define DEPRECATED(msg)
Definition deprecate.h:23
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
Definition kdev_t.h:24