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