cprover
report_util.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Bounded Model Checking Utilities
4 
5 Author: Daniel Kroening, Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
12 #include "report_util.h"
13 
14 #include <algorithm>
15 
16 #include <util/json.h>
17 #include <util/json_irep.h>
18 #include <util/string2int.h>
19 #include <util/ui_message.h>
20 #include <util/xml.h>
21 #include <util/xml_irep.h>
22 
24 
27 
29 #include "goto_trace_storage.h"
30 
31 #include "bmc_util.h"
32 
33 void report_success(ui_message_handlert &ui_message_handler)
34 {
35  messaget msg(ui_message_handler);
36  msg.result() << "VERIFICATION SUCCESSFUL" << messaget::eom;
37 
38  switch(ui_message_handler.get_ui())
39  {
41  break;
42 
44  {
45  xmlt xml("cprover-status");
46  xml.data = "SUCCESS";
47  msg.result() << xml;
48  }
49  break;
50 
52  {
53  json_objectt json_result;
54  json_result["cProverStatus"] = json_stringt("success");
55  msg.result() << json_result;
56  }
57  break;
58  }
59 }
60 
61 void report_failure(ui_message_handlert &ui_message_handler)
62 {
63  messaget msg(ui_message_handler);
64  msg.result() << "VERIFICATION FAILED" << messaget::eom;
65 
66  switch(ui_message_handler.get_ui())
67  {
69  break;
70 
72  {
73  xmlt xml("cprover-status");
74  xml.data = "FAILURE";
75  msg.result() << xml;
76  }
77  break;
78 
80  {
81  json_objectt json_result;
82  json_result["cProverStatus"] = json_stringt("failure");
83  msg.result() << json_result;
84  }
85  break;
86  }
87 }
88 
89 void report_inconclusive(ui_message_handlert &ui_message_handler)
90 {
91  messaget msg(ui_message_handler);
92  msg.result() << "VERIFICATION INCONCLUSIVE" << messaget::eom;
93 
94  switch(ui_message_handler.get_ui())
95  {
97  break;
98 
100  {
101  xmlt xml("cprover-status");
102  xml.data = "INCONCLUSIVE";
103  msg.result() << xml;
104  }
105  break;
106 
108  {
109  json_objectt json_result;
110  json_result["cProverStatus"] = json_stringt("inconclusive");
111  msg.result() << json_result;
112  }
113  break;
114  }
115 }
116 
117 void report_error(ui_message_handlert &ui_message_handler)
118 {
119  messaget msg(ui_message_handler);
120  msg.result() << "VERIFICATION ERROR" << messaget::eom;
121 
122  switch(ui_message_handler.get_ui())
123  {
125  break;
126 
128  {
129  xmlt xml("cprover-status");
130  xml.data = "ERROR";
131  msg.result() << xml;
132  }
133  break;
134 
136  {
137  json_objectt json_result;
138  json_result["cProverStatus"] = json_stringt("error");
139  msg.result() << json_result;
140  }
141  break;
142  }
143 }
144 
146  const irep_idt &property_id,
147  const property_infot &property_info,
148  messaget &log,
149  irep_idt current_file = irep_idt())
150 {
151  const auto &l = property_info.pc->source_location;
152  log.result() << messaget::faint << '[' << property_id << "] "
153  << messaget::reset;
154  if(l.get_file() != current_file)
155  log.result() << "file " << l.get_file() << ' ';
156  if(!l.get_line().empty())
157  log.result() << "line " << l.get_line() << ' ';
158  log.result() << property_info.description << ": ";
159  switch(property_info.status)
160  {
162  log.result() << messaget::magenta;
163  break;
165  log.result() << messaget::yellow;
166  break;
169  break;
171  log.result() << messaget::green;
172  break;
174  log.result() << messaget::red;
175  break;
177  log.result() << messaget::bright_red;
178  break;
179  }
180  log.result() << as_string(property_info.status) << messaget::reset
181  << messaget::eom;
182 }
183 
184 using propertyt = std::pair<irep_idt, property_infot>;
194 static bool
195 is_property_less_than(const propertyt &property1, const propertyt &property2)
196 {
197  const auto &p1 = property1.second.pc->source_location;
198  const auto &p2 = property2.second.pc->source_location;
199  if(p1.get_file() != p2.get_file())
200  return id2string(p1.get_file()) < id2string(p2.get_file());
201  if(p1.get_function() != p2.get_function())
202  return id2string(p1.get_function()) < id2string(p2.get_function());
203  else if(
204  !p1.get_line().empty() && !p2.get_line().empty() &&
205  p1.get_line() != p2.get_line())
206  return std::stoul(id2string(p1.get_line())) <
207  std::stoul(id2string(p2.get_line()));
208 
209  const auto split_property_id =
210  [](const irep_idt &property_id) -> std::pair<std::string, std::size_t> {
211  const auto property_string = id2string(property_id);
212  const auto last_dot = property_string.rfind('.');
213  std::string property_name;
214  std::string property_number;
215  if(last_dot == std::string::npos)
216  {
217  property_name = "";
218  property_number = property_string;
219  }
220  else
221  {
222  property_name = property_string.substr(0, last_dot);
223  property_number = property_string.substr(last_dot + 1);
224  }
225  const auto maybe_number = string2optional_size_t(property_number);
226  if(maybe_number.has_value())
227  return std::make_pair(property_name, *maybe_number);
228  else
229  return std::make_pair(property_name, 0);
230  };
231 
232  const auto left_split = split_property_id(property1.first);
233  const auto left_id_name = left_split.first;
234  const auto left_id_number = left_split.second;
235 
236  const auto right_split = split_property_id(property2.first);
237  const auto right_id_name = right_split.first;
238  const auto right_id_number = right_split.second;
239 
240  if(left_id_name != right_id_name)
241  return left_id_name < right_id_name;
242  else
243  return left_id_number < right_id_number;
244 }
245 
246 static std::vector<propertiest::const_iterator>
248 {
249  std::vector<propertiest::const_iterator> sorted_properties;
250  for(auto p_it = properties.begin(); p_it != properties.end(); p_it++)
251  sorted_properties.push_back(p_it);
252 
253  std::sort(
254  sorted_properties.begin(),
255  sorted_properties.end(),
256  [](propertiest::const_iterator pit1, propertiest::const_iterator pit2) {
257  return is_property_less_than(*pit1, *pit2);
258  });
259  return sorted_properties;
260 }
261 
263  const std::vector<propertiest::const_iterator> &sorted_properties,
264  messaget &log)
265 {
266  if(sorted_properties.empty())
267  return;
268 
269  log.result() << "\n** Results:" << messaget::eom;
270  // now show in the order we have determined
271  irep_idt previous_function;
272  irep_idt current_file;
273  for(const auto &p : sorted_properties)
274  {
275  const auto &l = p->second.pc->source_location;
276  if(l.get_function() != previous_function)
277  {
278  if(!previous_function.empty())
279  log.result() << '\n';
280  previous_function = l.get_function();
281  if(!previous_function.empty())
282  {
283  current_file = l.get_file();
284  if(!current_file.empty())
285  log.result() << current_file << ' ';
286  if(!l.get_function().empty())
287  log.result() << "function " << l.get_function();
288  log.result() << messaget::eom;
289  }
290  }
291  output_single_property_plain(p->first, p->second, log, current_file);
292  }
293 }
294 
295 static void output_iterations(
296  const propertiest &properties,
297  std::size_t iterations,
298  messaget &log)
299 {
300  if(properties.empty())
301  return;
302 
303  log.status() << "\n** "
304  << count_properties(properties, property_statust::FAIL) << " of "
305  << properties.size() << " failed (" << iterations
306  << " iterations)" << messaget::eom;
307 }
308 
310  const propertiest &properties,
311  std::size_t iterations,
312  ui_message_handlert &ui_message_handler)
313 {
314  messaget log(ui_message_handler);
315  switch(ui_message_handler.get_ui())
316  {
318  {
319  const auto sorted_properties = get_sorted_properties(properties);
320  output_properties_plain(sorted_properties, log);
321  output_iterations(properties, iterations, log);
322  break;
323  }
325  {
326  for(const auto &property_pair : properties)
327  {
328  log.result() << xml(property_pair.first, property_pair.second);
329  }
330  break;
331  }
333  {
334  json_stream_objectt &json_result =
335  ui_message_handler.get_json_stream().push_back_stream_object();
336  json_stream_arrayt &result_array =
337  json_result.push_back_stream_array("result");
338  for(const auto &property_pair : properties)
339  {
340  result_array.push_back(json(property_pair.first, property_pair.second));
341  }
342  break;
343  }
344  }
345 }
346 
348  const propertiest &properties,
349  const goto_trace_storaget &traces,
350  const trace_optionst &trace_options,
351  std::size_t iterations,
352  ui_message_handlert &ui_message_handler)
353 {
354  messaget log(ui_message_handler);
355  switch(ui_message_handler.get_ui())
356  {
358  {
359  const auto sorted_properties = get_sorted_properties(properties);
360  output_properties_plain(sorted_properties, log);
361  for(const auto &property_it : sorted_properties)
362  {
363  if(property_it->second.status == property_statust::FAIL)
364  {
365  log.result() << "\n"
366  << "Trace for " << property_it->first << ":"
367  << "\n";
369  log.result(),
370  traces.get_namespace(),
371  traces[property_it->first],
372  trace_options);
373  log.result() << messaget::eom;
374  }
375  }
376  output_iterations(properties, iterations, log);
377  break;
378  }
380  {
381  for(const auto &property_pair : properties)
382  {
383  xmlt xml_result = xml(property_pair.first, property_pair.second);
384  if(property_pair.second.status == property_statust::FAIL)
385  {
386  convert(
387  traces.get_namespace(),
388  traces[property_pair.first],
389  xml_result.new_element());
390  }
391  log.result() << xml_result;
392  }
393  break;
394  }
396  {
397  json_stream_objectt &json_result =
398  ui_message_handler.get_json_stream().push_back_stream_object();
399  json_stream_arrayt &result_array =
400  json_result.push_back_stream_array("result");
401  for(const auto &property_pair : properties)
402  {
403  json_stream_objectt &json_property =
404  result_array.push_back_stream_object();
405  json(json_property, property_pair.first, property_pair.second);
406  if(property_pair.second.status == property_statust::FAIL)
407  {
408  json_stream_arrayt &json_trace =
409  json_property.push_back_stream_array("trace");
410  convert<json_stream_arrayt>(
411  traces.get_namespace(),
412  traces[property_pair.first],
413  json_trace,
414  trace_options);
415  }
416  }
417  break;
418  }
419  }
420 }
421 
423  const fault_location_infot &fault_location,
424  messaget &log)
425 {
426  log.conditional_output(
427  log.debug(), [fault_location](messaget::mstreamt &out) {
428  out << "Fault localization scores:" << messaget::eom;
429  for(auto &score_pair : fault_location.scores)
430  {
431  out << score_pair.first->source_location
432  << "\n score: " << score_pair.second << messaget::eom;
433  }
434  });
435 }
436 
439 {
440  PRECONDITION(!fault_location.scores.empty());
441 
442  return std::max_element(
443  fault_location.scores.begin(),
444  fault_location.scores.end(),
445  [](
446  fault_location_infot::score_mapt::value_type score_pair1,
447  fault_location_infot::score_mapt::value_type score_pair2) {
448  return score_pair1.second < score_pair2.second;
449  })
450  ->first;
451 }
452 
454  const irep_idt &property_id,
455  const fault_location_infot &fault_location,
456  messaget &log)
457 {
458  if(fault_location.scores.empty())
459  {
460  log.result() << "[" + id2string(property_id) + "]: \n"
461  << " unable to localize fault" << messaget::eom;
462  return;
463  }
464 
465  output_fault_localization_scores(fault_location, log);
466  log.result() << "[" + id2string(property_id) + "]: \n "
467  << max_fault_localization_score(fault_location)->source_location
468  << messaget::eom;
469 }
470 
472  const std::unordered_map<irep_idt, fault_location_infot> &fault_locations,
473  messaget &log)
474 {
475  log.result() << "\n** Most likely fault location:" << messaget::eom;
476  for(const auto &fault_location_pair : fault_locations)
477  {
479  fault_location_pair.first, fault_location_pair.second, log);
480  }
481 }
482 
483 static xmlt xml(
484  const irep_idt &property_id,
485  const fault_location_infot &fault_location,
486  messaget &log)
487 {
488  xmlt xml_diagnosis("diagnosis");
489 
490  xml_diagnosis.set_attribute("property", id2string(property_id));
491 
492  if(fault_location.scores.empty())
493  {
494  xml_diagnosis.new_element("result").data = "unable to localize fault";
495  return xml_diagnosis;
496  }
497 
498  output_fault_localization_scores(fault_location, log);
499 
500  xmlt xml_location =
501  xml(max_fault_localization_score(fault_location)->source_location);
502  xml_diagnosis.new_element("result").new_element().swap(xml_location);
503 
504  return xml_diagnosis;
505 }
506 
508  const std::unordered_map<irep_idt, fault_location_infot> &fault_locations,
509  messaget &log)
510 {
511  xmlt dest("fault-localization");
512  for(const auto &fault_location_pair : fault_locations)
513  {
514  xmlt xml_diagnosis =
515  xml(fault_location_pair.first, fault_location_pair.second, log);
516  dest.new_element().swap(xml_diagnosis);
517  }
518  log.result() << dest;
519 }
520 
521 static json_objectt json(const fault_location_infot &fault_location)
522 {
523  json_objectt json_result;
524  if(fault_location.scores.empty())
525  {
526  json_result["result"] = json_stringt("unable to localize fault");
527  }
528  else
529  {
530  json_result["result"] =
531  json(max_fault_localization_score(fault_location)->source_location);
532  }
533  return json_result;
534 }
535 
537  const propertiest &properties,
538  const std::unordered_map<irep_idt, fault_location_infot> &fault_locations,
539  std::size_t iterations,
540  ui_message_handlert &ui_message_handler)
541 {
542  messaget log(ui_message_handler);
543  switch(ui_message_handler.get_ui())
544  {
546  {
547  output_properties(properties, iterations, ui_message_handler);
548  output_fault_localization_plain(fault_locations, log);
549  break;
550  }
552  {
553  json_stream_objectt &json_result =
554  ui_message_handler.get_json_stream().push_back_stream_object();
555  json_stream_arrayt &result_array =
556  json_result.push_back_stream_array("result");
557  for(const auto &property_pair : properties)
558  {
559  json_stream_objectt &json_property =
560  result_array.push_back_stream_object();
561  json(json_property, property_pair.first, property_pair.second);
562  if(property_pair.second.status == property_statust::FAIL)
563  {
564  json_property.push_back(
565  "diagnosis", json(fault_locations.at(property_pair.first)));
566  }
567  }
568  break;
569  }
571  {
572  output_properties(properties, iterations, ui_message_handler);
573  output_fault_localization_xml(fault_locations, log);
574  break;
575  }
576  }
577 }
578 
580  const propertiest &properties,
581  const goto_trace_storaget &traces,
582  const trace_optionst &trace_options,
583  const std::unordered_map<irep_idt, fault_location_infot> &fault_locations,
584  std::size_t iterations,
585  ui_message_handlert &ui_message_handler)
586 {
587  messaget log(ui_message_handler);
588  switch(ui_message_handler.get_ui())
589  {
591  {
593  properties, traces, trace_options, iterations, ui_message_handler);
594  output_fault_localization_plain(fault_locations, log);
595  break;
596  }
598  {
599  json_stream_objectt &json_result =
600  ui_message_handler.get_json_stream().push_back_stream_object();
601  json_stream_arrayt &result_array =
602  json_result.push_back_stream_array("result");
603  for(const auto &property_pair : properties)
604  {
605  json_stream_objectt &json_property =
606  result_array.push_back_stream_object();
607  json(json_property, property_pair.first, property_pair.second);
608  if(property_pair.second.status == property_statust::FAIL)
609  {
610  json_stream_arrayt &json_trace =
611  json_property.push_back_stream_array("trace");
612  convert<json_stream_arrayt>(
613  traces.get_namespace(),
614  traces[property_pair.first],
615  json_trace,
616  trace_options);
617  json_property.push_back(
618  "diagnosis", json(fault_locations.at(property_pair.first)));
619  }
620  }
621  break;
622  }
624  {
626  properties, traces, trace_options, iterations, ui_message_handler);
627  output_fault_localization_xml(fault_locations, log);
628  break;
629  }
630  }
631 }
632 
634  const goto_tracet &goto_trace,
635  const namespacet &ns,
636  const trace_optionst &trace_options,
637  const fault_location_infot &fault_location_info,
638  ui_message_handlert &ui_message_handler)
639 {
640  messaget log(ui_message_handler);
641  switch(ui_message_handler.get_ui())
642  {
644  output_error_trace(goto_trace, ns, trace_options, ui_message_handler);
646  goto_trace.get_last_step().property_id, fault_location_info, log);
647  break;
648 
650  {
651  json_stream_objectt &json_result =
652  ui_message_handler.get_json_stream().push_back_stream_object();
653  const goto_trace_stept &step = goto_trace.get_last_step();
654  json_result["property"] = json_stringt(step.property_id);
655  json_result["description"] = json_stringt(step.comment);
656  json_result["status"] = json_stringt("failed");
657  json_stream_arrayt &json_trace =
658  json_result.push_back_stream_array("trace");
659  convert<json_stream_arrayt>(ns, goto_trace, json_trace, trace_options);
660  json_result.push_back("diagnosis", json(fault_location_info));
661  break;
662  }
663 
665  {
666  output_error_trace(goto_trace, ns, trace_options, ui_message_handler);
667  xmlt dest(
668  "fault-localization",
669  {},
670  {xml(goto_trace.get_last_step().property_id, fault_location_info, log)});
671  log.result() << dest;
672  break;
673  }
674  }
675 }
676 
678  resultt result,
679  ui_message_handlert &ui_message_handler)
680 {
681  switch(result)
682  {
683  case resultt::PASS:
684  report_success(ui_message_handler);
685  break;
686  case resultt::FAIL:
687  report_failure(ui_message_handler);
688  break;
689  case resultt::UNKNOWN:
690  report_inconclusive(ui_message_handler);
691  break;
692  case resultt::ERROR:
693  report_error(ui_message_handler);
694  break;
695  }
696 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
propertiest
std::unordered_map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition: properties.h:75
property_statust::FAIL
@ FAIL
The property was violated.
json
static json_objectt json(const fault_location_infot &fault_location)
Definition: report_util.cpp:521
goto_trace_stept::comment
std::string comment
Definition: goto_trace.h:123
output_single_property_plain
static void output_single_property_plain(const irep_idt &property_id, const property_infot &property_info, messaget &log, irep_idt current_file=irep_idt())
Definition: report_util.cpp:145
ui_message_handlert
Definition: ui_message.h:20
property_statust::ERROR
@ ERROR
An error occurred during goto checking.
messaget::reset
static const commandt reset
return to default formatting, as defined by the terminal
Definition: message.h:343
resultt
resultt
The result of goto verifying.
Definition: properties.h:44
ui_message_handlert::uit::XML_UI
@ XML_UI
get_sorted_properties
static std::vector< propertiest::const_iterator > get_sorted_properties(const propertiest &properties)
Definition: report_util.cpp:247
messaget::status
mstreamt & status() const
Definition: message.h:414
output_properties_with_traces
void output_properties_with_traces(const propertiest &properties, const goto_trace_storaget &traces, const trace_optionst &trace_options, std::size_t iterations, ui_message_handlert &ui_message_handler)
Definition: report_util.cpp:347
output_fault_localization_xml
static void output_fault_localization_xml(const std::unordered_map< irep_idt, fault_location_infot > &fault_locations, messaget &log)
Definition: report_util.cpp:507
messaget::bright_red
static const commandt bright_red
render text with bright red foreground color
Definition: message.h:364
report_inconclusive
void report_inconclusive(ui_message_handlert &ui_message_handler)
Definition: report_util.cpp:89
xml_irep.h
fault_location_infot
Definition: fault_localization_provider.h:23
resultt::PASS
@ PASS
No properties were violated.
output_error_trace_with_fault_localization
void output_error_trace_with_fault_localization(const goto_tracet &goto_trace, const namespacet &ns, const trace_optionst &trace_options, const fault_location_infot &fault_location_info, ui_message_handlert &ui_message_handler)
Definition: report_util.cpp:633
irep_idt
dstringt irep_idt
Definition: irep.h:32
messaget::eom
static eomt eom
Definition: message.h:297
output_properties
void output_properties(const propertiest &properties, std::size_t iterations, ui_message_handlert &ui_message_handler)
Definition: report_util.cpp:309
resultt::UNKNOWN
@ UNKNOWN
No property was violated, neither was there an error.
goto_trace_stept
Step of the trace of a GOTO program.
Definition: goto_trace.h:50
property_statust::NOT_REACHABLE
@ NOT_REACHABLE
The property was proven to be unreachable.
xml.h
json_irep.h
Util.
property_infot::description
std::string description
A description (usually derived from the assertion's comment)
Definition: properties.h:68
resultt::FAIL
@ FAIL
Some properties were violated.
json_objectt
Definition: json.h:300
ui_message_handlert::get_ui
virtual uit get_ui() const
Definition: ui_message.h:31
json_stream_objectt::push_back_stream_array
json_stream_arrayt & push_back_stream_array(const std::string &key)
Add a JSON array stream for a specific key.
Definition: json_stream.cpp:120
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
ui_message_handlert::get_json_stream
virtual json_stream_arrayt & get_json_stream()
Definition: ui_message.h:38
string2int.h
bmc_util.h
Bounded Model Checking Utilities.
property_infot::status
property_statust status
The status of the property.
Definition: properties.h:71
messaget::green
static const commandt green
render text with green foreground color
Definition: message.h:349
convert
static bool convert(const irep_idt &identifier, const std::ostringstream &s, symbol_tablet &symbol_table, message_handlert &message_handler)
Definition: builtin_factory.cpp:42
messaget::result
mstreamt & result() const
Definition: message.h:409
messaget::faint
static const commandt faint
render text with faint font
Definition: message.h:385
fault_location_infot::scores
score_mapt scores
Definition: fault_localization_provider.h:25
messaget::yellow
static const commandt yellow
render text with yellow foreground color
Definition: message.h:352
output_properties_with_fault_localization
void output_properties_with_fault_localization(const propertiest &properties, const std::unordered_map< irep_idt, fault_location_infot > &fault_locations, std::size_t iterations, ui_message_handlert &ui_message_handler)
Definition: report_util.cpp:536
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
ui_message_handlert::uit::JSON_UI
@ JSON_UI
report_error
void report_error(ui_message_handlert &ui_message_handler)
Definition: report_util.cpp:117
output_overall_result
void output_overall_result(resultt result, ui_message_handlert &ui_message_handler)
Definition: report_util.cpp:677
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
xml_goto_trace.h
Traces of GOTO Programs.
report_failure
void report_failure(ui_message_handlert &ui_message_handler)
Definition: report_util.cpp:61
json_stream_arrayt
Provides methods for streaming JSON arrays.
Definition: json_stream.h:93
goto_trace_storage.h
Goto Trace Storage.
property_statust::NOT_CHECKED
@ NOT_CHECKED
The property was not checked (also used for initialization)
dstringt::empty
bool empty() const
Definition: dstring.h:88
count_properties
std::size_t count_properties(const propertiest &properties, property_statust status)
Return the number of properties with given status.
Definition: properties.cpp:157
string2optional_size_t
optionalt< std::size_t > string2optional_size_t(const std::string &str, int base)
Convert string to size_t similar to the stoul or stoull functions, return nullopt when the conversion...
Definition: string2int.cpp:72
json_goto_trace.h
Traces of GOTO Programs.
output_iterations
static void output_iterations(const propertiest &properties, std::size_t iterations, messaget &log)
Definition: report_util.cpp:295
xmlt
Definition: xml.h:21
output_fault_localization_scores
void output_fault_localization_scores(const fault_location_infot &fault_location, messaget &log)
Definition: report_util.cpp:422
resultt::ERROR
@ ERROR
An error occurred during goto checking.
output_fault_localization_plain
static void output_fault_localization_plain(const irep_idt &property_id, const fault_location_infot &fault_location, messaget &log)
Definition: report_util.cpp:453
property_statust::UNKNOWN
@ UNKNOWN
The checker was unable to determine the status of the property.
goto_trace_storaget
Definition: goto_trace_storage.h:18
propertyt
std::pair< irep_idt, property_infot > propertyt
Definition: report_util.cpp:184
output_properties_with_traces_and_fault_localization
void output_properties_with_traces_and_fault_localization(const propertiest &properties, const goto_trace_storaget &traces, const trace_optionst &trace_options, const std::unordered_map< irep_idt, fault_location_infot > &fault_locations, std::size_t iterations, ui_message_handlert &ui_message_handler)
Definition: report_util.cpp:579
json_stream_arrayt::push_back_stream_object
json_stream_objectt & push_back_stream_object()
Add a JSON object child stream.
Definition: json_stream.cpp:82
goto_trace_stept::property_id
irep_idt property_id
Definition: goto_trace.h:122
json_stream_objectt
Provides methods for streaming JSON objects.
Definition: json_stream.h:140
property_infot
Definition: properties.h:58
report_success
void report_success(ui_message_handlert &ui_message_handler)
Definition: report_util.cpp:33
show_goto_trace
void show_goto_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options)
Output the trace on the given stream out.
Definition: goto_trace.cpp:767
messaget::red
static const commandt red
render text with red foreground color
Definition: message.h:346
fault_localization_provider.h
Interface for Goto Checkers to provide Fault Localization.
max_fault_localization_score
static goto_programt::const_targett max_fault_localization_score(const fault_location_infot &fault_location)
Definition: report_util.cpp:438
trace_optionst
Options for printing the trace using show_goto_trace.
Definition: goto_trace.h:215
ui_message_handlert::uit::PLAIN
@ PLAIN
goto_trace_storaget::get_namespace
const namespacet & get_namespace() const
Definition: goto_trace_storage.cpp:60
xmlt::set_attribute
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:175
is_property_less_than
static bool is_property_less_than(const propertyt &property1, const propertyt &property2)
Compare two properties according to the following sort:
Definition: report_util.cpp:195
json_streamt::first
bool first
Is the current element the first element in the object or array? This is required to know whether a d...
Definition: json_stream.h:68
report_util.h
Bounded Model Checking Utilities.
output_properties_plain
static void output_properties_plain(const std::vector< propertiest::const_iterator > &sorted_properties, messaget &log)
Definition: report_util.cpp:262
as_string
std::string as_string(resultt result)
Definition: properties.cpp:20
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
build_goto_trace.h
Traces of GOTO Programs.
json.h
output_error_trace
void output_error_trace(const goto_tracet &goto_trace, const namespacet &ns, const trace_optionst &trace_options, ui_message_handlert &ui_message_handler)
Definition: bmc_util.cpp:65
xmlt::swap
void swap(xmlt &xml)
Definition: xml.cpp:25
goto_tracet
Trace of a GOTO program.
Definition: goto_trace.h:171
property_statust::PASS
@ PASS
The property was not violated.
messaget::mstreamt
Definition: message.h:224
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
messaget::debug
mstreamt & debug() const
Definition: message.h:429
goto_tracet::get_last_step
goto_trace_stept & get_last_step()
Retrieves the final step in the trace for manipulation (used to fill a trace from code,...
Definition: goto_trace.h:199
messaget::bright_green
static const commandt bright_green
render text with bright green foreground color
Definition: message.h:367
json_stream_arrayt::push_back
void push_back(const jsont &json)
Push back a JSON element into the current array stream.
Definition: json_stream.h:106
xmlt::data
std::string data
Definition: xml.h:39
property_infot::pc
goto_programt::const_targett pc
A pointer to the corresponding goto instruction.
Definition: properties.h:65
messaget::magenta
static const commandt magenta
render text with magenta foreground color
Definition: message.h:358
json_stream_objectt::push_back
void push_back(const std::string &key, const jsont &json)
Push back a JSON element into the current object stream.
Definition: json_stream.h:178
xml
static xmlt xml(const irep_idt &property_id, const fault_location_infot &fault_location, messaget &log)
Definition: report_util.cpp:483
xmlt::new_element
xmlt & new_element(const std::string &key)
Definition: xml.h:95
json_stringt
Definition: json.h:270
ui_message.h