cprover
ui_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 #include "ui_message.h"
10 
11 #include <fstream>
12 #include <iostream>
13 
14 #include "xml.h"
15 #include "json.h"
16 #include "xml_expr.h"
17 #include "cout_message.h"
18 #include "cmdline.h"
19 
21  uit __ui, const std::string &program):_ui(__ui)
22 {
23  switch(__ui)
24  {
25  case uit::PLAIN:
26  break;
27 
28  case uit::XML_UI:
29  std::cout << "<?xml version=\"1.0\" encoding=\"UTF-8\"?>" << "\n";
30  std::cout << "<cprover>" << "\n";
31 
32  {
33  xmlt program_xml;
34  program_xml.name="program";
35  program_xml.data=program;
36 
37  std::cout << program_xml;
38  }
39  break;
40 
41  case uit::JSON_UI:
42  {
43  std::cout << "[\n";
44  json_objectt json_program;
45  json_program["program"] = json_stringt(program);
46  std::cout << json_program;
47  }
48  break;
49  }
50 }
51 
53  const class cmdlinet &cmdline,
54  const std::string &program):
56  cmdline.isset("xml-ui")?uit::XML_UI:
57  cmdline.isset("json-ui")?uit::JSON_UI:
58  uit::PLAIN,
59  program)
60 {
61 }
62 
64 {
65  switch(get_ui())
66  {
67  case uit::XML_UI:
68  std::cout << "</cprover>" << "\n";
69  break;
70 
71  case uit::JSON_UI:
72  std::cout << "\n]\n";
73  break;
74 
75  case uit::PLAIN:
76  break;
77  }
78 }
79 
80 const char *ui_message_handlert::level_string(unsigned level)
81 {
82  if(level==1)
83  return "ERROR";
84  else if(level==2)
85  return "WARNING";
86  else
87  return "STATUS-MESSAGE";
88 }
89 
91  unsigned level,
92  const std::string &message)
93 {
94  if(verbosity>=level)
95  {
96  switch(get_ui())
97  {
98  case uit::PLAIN:
99  {
100  console_message_handlert console_message_handler;
101  console_message_handler.print(level, message);
102  }
103  break;
104 
105  case uit::XML_UI:
106  case uit::JSON_UI:
107  {
108  source_locationt location;
109  location.make_nil();
110  print(level, message, -1, location);
111  }
112  break;
113  }
114  }
115 }
116 
118  unsigned level,
119  const std::string &message,
120  int sequence_number,
121  const source_locationt &location)
122 {
123  message_handlert::print(level, message);
124 
125  if(verbosity>=level)
126  {
127  switch(get_ui())
128  {
129  case uit::PLAIN:
131  level, message, sequence_number, location);
132  break;
133 
134  case uit::XML_UI:
135  case uit::JSON_UI:
136  {
137  std::string tmp_message(message);
138 
139  if(!tmp_message.empty() && *tmp_message.rbegin()=='\n')
140  tmp_message.resize(tmp_message.size()-1);
141 
142  const char *type=level_string(level);
143 
144  std::string sequence_number_str=
145  sequence_number>=0?std::to_string(sequence_number):"";
146 
147  ui_msg(type, tmp_message, sequence_number_str, location);
148  }
149  break;
150  }
151  }
152 }
153 
155  const std::string &type,
156  const std::string &msg1,
157  const std::string &msg2,
158  const source_locationt &location)
159 {
160  switch(get_ui())
161  {
162  case uit::PLAIN:
163  break;
164 
165  case uit::XML_UI:
166  xml_ui_msg(type, msg1, msg2, location);
167  break;
168 
169  case uit::JSON_UI:
170  json_ui_msg(type, msg1, msg2, location);
171  break;
172  }
173 }
174 
176  const std::string &type,
177  const std::string &msg1,
178  const std::string &msg2,
179  const source_locationt &location)
180 {
181  xmlt result;
182  result.name="message";
183 
184  if(location.is_not_nil() &&
185  !location.get_file().empty())
186  result.new_element(xml(location));
187 
188  result.new_element("text").data=msg1;
189  result.set_attribute("type", type);
190 
191  std::cout << result;
192  std::cout << '\n';
193 }
194 
196  const std::string &type,
197  const std::string &msg1,
198  const std::string &msg2,
199  const source_locationt &location)
200 {
201  json_objectt result;
202 
203  #if 0
204  if(location.is_not_nil() &&
205  !location.get_file().empty())
206  result.new_element(xml(location));
207  #endif
208 
209  result["messageType"] = json_stringt(type);
210  result["messageText"] = json_stringt(msg1);
211 
212  // By convention a leading comma is created by every new array entry.
213  // The first entry is generated in the constructor and does not have
214  // a trailing comma.
215  std::cout << ",\n" << result;
216 }
217 
218 void ui_message_handlert::flush(unsigned level)
219 {
220  switch(get_ui())
221  {
222  case uit::PLAIN:
223  {
224  console_message_handlert console_message_handler;
225  console_message_handler.flush(level);
226  }
227  break;
228 
229  case uit::XML_UI:
230  case uit::JSON_UI:
231  {
232  std::cout << std::flush;
233  }
234  break;
235  }
236 }
bool is_not_nil() const
Definition: irep.h:104
uit get_ui() const
Definition: ui_message.h:29
std::string name
Definition: xml.h:30
const char * level_string(unsigned level)
Definition: ui_message.cpp:80
unsigned verbosity
Definition: message.h:56
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:25
virtual void flush(unsigned level)
Definition: ui_message.cpp:218
virtual void json_ui_msg(const std::string &type, const std::string &msg1, const std::string &msg2, const source_locationt &location)
Definition: ui_message.cpp:195
virtual void flush(unsigned level) override
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:174
virtual void xml_ui_msg(const std::string &type, const std::string &msg1, const std::string &msg2, const source_locationt &location)
Definition: ui_message.cpp:175
Definition: xml.h:18
std::string data
Definition: xml.h:30
virtual void ui_msg(const std::string &type, const std::string &msg1, const std::string &msg2, const source_locationt &location)
Definition: ui_message.cpp:154
xmlt & new_element(const std::string &name)
Definition: xml.h:86
const irep_idt & get_file() const
virtual ~ui_message_handlert()
Definition: ui_message.cpp:63
virtual void print(unsigned level, const std::string &message)
Definition: ui_message.cpp:90
void make_nil()
Definition: irep.h:243
virtual void print(unsigned level, const std::string &message) override
bool empty() const
Definition: dstring.h:61
virtual void print(unsigned level, const std::string &message)=0
Definition: message.cpp:57