cprover
message.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_UTIL_MESSAGE_H
11 #define CPROVER_UTIL_MESSAGE_H
12 
13 #include <string>
14 #include <iosfwd>
15 #include <sstream>
16 
17 #include "invariant.h"
18 #include "source_location.h"
19 
21 {
22 public:
24  {
25  }
26 
27  virtual void print(unsigned level, const std::string &message) = 0;
28 
29  virtual void print(
30  unsigned level,
31  const std::string &message,
32  int sequence_number,
33  const source_locationt &location);
34 
35  virtual void flush(unsigned level)
36  {
37  // no-op by default
38  }
39 
41  {
42  }
43 
44  void set_verbosity(unsigned _verbosity) { verbosity=_verbosity; }
45  unsigned get_verbosity() const { return verbosity; }
46 
47  unsigned get_message_count(unsigned level) const
48  {
49  if(level>=message_count.size())
50  return 0;
51 
52  return message_count[level];
53  }
54 
55 protected:
56  unsigned verbosity;
57  std::vector<unsigned> message_count;
58 };
59 
61 {
62 public:
63  virtual void print(unsigned level, const std::string &message)
64  {
65  message_handlert::print(level, message);
66  }
67 
68  virtual void print(
69  unsigned level,
70  const std::string &message,
71  int sequence_number,
72  const source_locationt &location)
73  {
74  print(level, message);
75  }
76 };
77 
79 {
80 public:
81  explicit stream_message_handlert(std::ostream &_out):out(_out)
82  {
83  }
84 
85  virtual void print(unsigned level, const std::string &message)
86  {
87  message_handlert::print(level, message);
88 
89  if(verbosity>=level)
90  out << message << '\n';
91  }
92 
93  virtual void flush(unsigned level)
94  {
95  out << std::flush;
96  }
97 
98 protected:
99  std::ostream &out;
100 };
101 
102 class messaget
103 {
104 public:
105  // Standard message levels:
106  //
107  // 0 none
108  // 1 only errors
109  // 2 + warnings
110  // 4 + results
111  // 6 + status/phase information
112  // 8 + statistical information
113  // 9 + progress information
114  // 10 + debug info
115 
117  {
118  M_ERROR=1, M_WARNING=2, M_RESULT=4, M_STATUS=6,
119  M_STATISTICS=8, M_PROGRESS=9, M_DEBUG=10
120  };
121 
122  virtual void set_message_handler(message_handlert &_message_handler)
123  {
124  message_handler=&_message_handler;
125  }
126 
128  {
129  INVARIANT(message_handler!=nullptr, "message handler is set");
130  return *message_handler;
131  }
132 
133  // constructors, destructor
134 
136  message_handler(nullptr),
137  mstream(M_DEBUG, *this)
138  {
139  }
140 
141  messaget(const messaget &other):
142  message_handler(other.message_handler),
143  mstream(other.mstream)
144  {
145  }
146 
147  explicit messaget(message_handlert &_message_handler):
148  message_handler(&_message_handler),
149  mstream(M_DEBUG, *this)
150  {
151  }
152 
153  virtual ~messaget();
154 
155  class mstreamt:public std::ostringstream
156  {
157  public:
159  unsigned _message_level,
160  messaget &_message):
161  message_level(_message_level),
162  message(_message)
163  {
164  }
165 
166  mstreamt(const mstreamt &other):
167  message_level(other.message_level),
168  message(other.message),
169  source_location(other.source_location)
170  {
171  }
172 
173  unsigned message_level;
176 
177  template <class T>
178  mstreamt &operator << (const T &x)
179  {
180  static_cast<std::ostream &>(*this) << x;
181  return *this;
182  }
183 
184  // for feeding in manipulator functions such as eom
186  {
187  return func(*this);
188  }
189  };
190 
191  // Feeding 'eom' into the stream triggers
192  // the printing of the message
193  static mstreamt &eom(mstreamt &m)
194  {
196  {
198  m.message_level,
199  m.str(),
200  -1,
201  m.source_location);
203  }
204  m.clear(); // clears error bits
205  m.str(std::string()); // clears the string
207  return m;
208  }
209 
210  // in lieu of std::endl
211  static mstreamt &endl(mstreamt &m)
212  {
213  static_cast<std::ostream &>(m) << std::endl;
214  return m;
215  }
216 
217  mstreamt &get_mstream(unsigned message_level)
218  {
219  mstream.message_level=message_level;
220  return mstream;
221  }
222 
224  {
225  return get_mstream(M_ERROR);
226  }
227 
229  {
230  return get_mstream(M_WARNING);
231  }
232 
234  {
235  return get_mstream(M_RESULT);
236  }
237 
239  {
240  return get_mstream(M_STATUS);
241  }
242 
244  {
245  return get_mstream(M_STATISTICS);
246  }
247 
249  {
250  return get_mstream(M_PROGRESS);
251  }
252 
254  {
255  return get_mstream(M_DEBUG);
256  }
257 
258 protected:
261 };
262 
263 #endif // CPROVER_UTIL_MESSAGE_H
mstreamt & warning()
Definition: message.h:228
mstreamt & result()
Definition: message.h:233
std::ostream & operator<<(std::ostream &out, const cfg_dominators_templatet< P, T, post_dom > &cfg_dominators)
Print the result of the dominator computation.
mstreamt & status()
Definition: message.h:238
stream_message_handlert(std::ostream &_out)
Definition: message.h:81
unsigned verbosity
Definition: message.h:56
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
virtual void print(unsigned level, const std::string &message)
Definition: message.h:85
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:202
unsigned get_verbosity() const
Definition: message.h:45
messaget(const messaget &other)
Definition: message.h:141
mstreamt & get_mstream(unsigned message_level)
Definition: message.h:217
std::ostream & out
Definition: message.h:99
source_locationt source_location
Definition: message.h:175
messaget & message
Definition: message.h:174
messaget()
Definition: message.h:135
virtual void print(unsigned level, const std::string &message, int sequence_number, const source_locationt &location)
Definition: message.h:68
static mstreamt & endl(mstreamt &m)
Definition: message.h:211
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:122
message_levelt
Definition: message.h:116
virtual void print(unsigned level, const std::string &message)
Definition: message.h:63
virtual void flush(unsigned level)
Definition: message.h:35
mstreamt & statistics()
Definition: message.h:243
messaget(message_handlert &_message_handler)
Definition: message.h:147
mstreamt & debug()
Definition: message.h:253
message_handlert & get_message_handler()
Definition: message.h:127
std::vector< unsigned > message_count
Definition: message.h:57
void clear()
Definition: irep.h:241
mstreamt(unsigned _message_level, messaget &_message)
Definition: message.h:158
mstreamt & error()
Definition: message.h:223
mstreamt & progress()
Definition: message.h:248
void set_verbosity(unsigned _verbosity)
Definition: message.h:44
virtual ~message_handlert()
Definition: message.h:40
virtual void flush(unsigned level)
Definition: message.h:93
mstreamt mstream
Definition: message.h:260
message_handlert * message_handler
Definition: message.h:259
unsigned message_level
Definition: message.h:173
mstreamt(const mstreamt &other)
Definition: message.h:166
virtual void print(unsigned level, const std::string &message)=0
Definition: message.cpp:57
unsigned get_message_count(unsigned level) const
Definition: message.h:47