cprover
message.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #include "message.h"
11 
12 #include "json.h"
13 #include "string2int.h"
14 
16  unsigned level,
17  const std::string &message,
18  const source_locationt &location)
19 {
20  std::string dest;
21 
22  const irep_idt &file=location.get_file();
23  const irep_idt &line=location.get_line();
24  const irep_idt &column=location.get_column();
25  const irep_idt &function=location.get_function();
26 
27  if(!file.empty())
28  {
29  if(!dest.empty())
30  dest+=' ';
31  dest+="file "+id2string(file);
32  }
33  if(!line.empty())
34  {
35  if(!dest.empty())
36  dest+=' ';
37  dest+="line "+id2string(line);
38  }
39  if(!column.empty())
40  {
41  if(!dest.empty())
42  dest+=' ';
43  dest+="column "+id2string(column);
44  }
45  if(!function.empty())
46  {
47  if(!dest.empty())
48  dest+=' ';
49  dest+="function "+id2string(function);
50  }
51 
52  if(!dest.empty())
53  dest+=": ";
54  dest+=message;
55 
56  print(level, dest);
57 }
58 
60  unsigned level,
61  const std::string &)
62 {
63  if(level>=message_count.size())
64  message_count.resize(level+1, 0);
65  ++message_count[level];
66 }
67 void message_handlert::print(unsigned level, const structured_datat &data)
68 {
69  // default to just printing out the data in a format
70  print(level, to_pretty(data));
71 }
72 
74 {
75 }
76 
77 // Visual studio requires this (empty) static object
79 
97 
105  const std::string &user_input,
106  const message_levelt default_verbosity,
107  message_handlert &dest)
108 {
109  unsigned v = default_verbosity;
110 
111  if(!user_input.empty())
112  {
113  v = unsafe_string2unsigned(user_input);
114 
115  if(v > messaget::M_DEBUG)
116  {
117  dest.print(
119  "verbosity value " + user_input + " out of range, using debug-level (" +
120  std::to_string(messaget::M_DEBUG) + ") verbosity",
121  source_locationt());
122 
123  v = messaget::M_DEBUG;
124  }
125  }
126 
127  dest.set_verbosity(v);
128 
129  return v;
130 }
131 
139  mstreamt &message_stream,
140  const std::function<void(mstreamt &)> &output_generator) const
141 {
142  if(
143  message_handler &&
144  message_handler->get_verbosity() >= message_stream.message_level)
145  {
146  output_generator(mstream);
147  }
148 }
149 
151 {
152  if(this->tellp() > 0)
153  *this << eom; // force end of previous message
155  {
157  }
158  return *this;
159 }
to_pretty
std::string to_pretty(const structured_datat &data)
Convert the structured_data into plain text.
Definition: structured_data.cpp:149
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
source_locationt::get_function
const irep_idt & get_function() const
Definition: source_location.h:56
messaget::reset
static const commandt reset
return to default formatting, as defined by the terminal
Definition: message.h:343
message_handlert::get_verbosity
unsigned get_verbosity() const
Definition: message.h:54
data
Definition: kdev_t.h:24
file
Definition: kdev_t.h:19
source_locationt::get_column
const irep_idt & get_column() const
Definition: source_location.h:51
messaget::bright_red
static const commandt bright_red
render text with bright red foreground color
Definition: message.h:364
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
messaget::eom
static eomt eom
Definition: message.h:297
messaget::italic
static const commandt italic
render italic text
Definition: message.h:388
source_locationt::get_line
const irep_idt & get_line() const
Definition: source_location.h:46
messaget::mstreamt::operator<<
mstreamt & operator<<(const xmlt &data)
Definition: message.h:249
message_handlert::print
virtual void print(unsigned level, const std::string &message)=0
Definition: message.cpp:59
json_objectt
Definition: json.h:300
messaget::bright_magenta
static const commandt bright_magenta
render text with bright magenta foreground color
Definition: message.h:376
message
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
Definition: static_verifier.cpp:74
string2int.h
message.h
messaget::bright_yellow
static const commandt bright_yellow
render text with bright yellow foreground color
Definition: message.h:370
messaget::green
static const commandt green
render text with green foreground color
Definition: message.h:349
messaget::faint
static const commandt faint
render text with faint font
Definition: message.h:385
messaget::bold
static const commandt bold
render text with bold font
Definition: message.h:382
messaget::yellow
static const commandt yellow
render text with yellow foreground color
Definition: message.h:352
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
message_handlert
Definition: message.h:28
dstringt::empty
bool empty() const
Definition: dstring.h:88
messaget::eomt
Definition: message.h:294
structured_datat
A way of representing nested key/value data.
Definition: structured_data.h:74
messaget::mstreamt::message
messaget & message
Definition: message.h:246
source_locationt
Definition: source_location.h:20
message_handlert::set_verbosity
void set_verbosity(unsigned _verbosity)
Definition: message.h:53
message_handlert::message_count
std::vector< std::size_t > message_count
Definition: message.h:73
messaget::message_handler
message_handlert * message_handler
Definition: message.h:439
messaget::M_WARNING
@ M_WARNING
Definition: message.h:170
messaget::red
static const commandt red
render text with red foreground color
Definition: message.h:346
messaget::message_levelt
message_levelt
Definition: message.h:169
messaget::conditional_output
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:138
unsafe_string2unsigned
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:38
json.h
messaget::~messaget
virtual ~messaget()
Definition: message.cpp:73
source_locationt::get_file
const irep_idt & get_file() const
Definition: source_location.h:36
messaget::underline
static const commandt underline
render underlined text
Definition: message.h:391
messaget::mstreamt
Definition: message.h:224
messaget::cyan
static const commandt cyan
render text with cyan foreground color
Definition: message.h:361
messaget::M_DEBUG
@ M_DEBUG
Definition: message.h:171
messaget::mstream
mstreamt mstream
Definition: message.h:440
messaget::bright_green
static const commandt bright_green
render text with bright green foreground color
Definition: message.h:367
messaget::eval_verbosity
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:104
messaget::mstreamt::message_level
unsigned message_level
Definition: message.h:245
messaget::magenta
static const commandt magenta
render text with magenta foreground color
Definition: message.h:358
messaget::bright_cyan
static const commandt bright_cyan
render text with bright cyan foreground color
Definition: message.h:379
messaget::bright_blue
static const commandt bright_blue
render text with bright blue foreground color
Definition: message.h:373
messaget::commandt
Definition: message.h:317
messaget::blue
static const commandt blue
render text with blue foreground color
Definition: message.h:355