cprover
cover_goals_report_util.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Cover Goals Reporting Utilities
4 
5 Author: Daniel Kroening, Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <iomanip>
15 
16 #include <util/json.h>
17 #include <util/json_irep.h>
18 #include <util/json_stream.h>
19 #include <util/ui_message.h>
20 #include <util/xml.h>
21 #include <util/xml_irep.h>
22 
24  const propertiest &properties,
25  unsigned iterations,
26  messaget &log)
27 {
28  const std::size_t goals_covered =
30  log.status() << "** " << goals_covered << " of " << properties.size()
31  << " covered (" << std::fixed << std::setw(1)
32  << std::setprecision(1)
33  << (properties.empty()
34  ? 100.0
35  : 100.0 * goals_covered / properties.size())
36  << "%)" << messaget::eom;
37  log.statistics() << "** Used " << iterations << " iteration"
38  << (iterations == 1 ? "" : "s") << messaget::eom;
39 }
40 
41 static void output_goals_plain(const propertiest &properties, messaget &log)
42 {
43  log.result() << "\n** coverage results:" << messaget::eom;
44 
45  for(const auto &property_pair : properties)
46  {
47  log.result() << "[" << property_pair.first << "]";
48 
49  if(property_pair.second.pc->source_location().is_not_nil())
50  log.result() << ' ' << property_pair.second.pc->source_location();
51 
52  if(!property_pair.second.description.empty())
53  log.result() << ' ' << property_pair.second.description;
54 
55  log.result() << ": "
56  << (property_pair.second.status == property_statust::FAIL
57  ? "SATISFIED"
58  : "FAILED")
59  << '\n';
60  }
61 
62  log.result() << messaget::eom;
63 }
64 
65 static void output_goals_xml(const propertiest &properties, messaget &log)
66 {
67  for(const auto &property_pair : properties)
68  {
69  xmlt xml_result(
70  "goal",
71  {{"id", id2string(property_pair.first)},
72  {"description", property_pair.second.description},
73  {"status",
74  property_pair.second.status == property_statust::FAIL ? "SATISFIED"
75  : "FAILED"}},
76  {});
77 
78  if(property_pair.second.pc->source_location().is_not_nil())
79  xml_result.new_element() =
80  xml(property_pair.second.pc->source_location());
81 
82  log.result() << xml_result;
83  }
84 }
85 
86 static void output_goals_json(
87  const propertiest &properties,
88  messaget &log,
89  ui_message_handlert &ui_message_handler)
90 {
91  if(log.status().tellp() > 0)
92  log.status() << messaget::eom; // force end of previous message
93  json_stream_objectt &json_result =
94  ui_message_handler.get_json_stream().push_back_stream_object();
95  json_stream_arrayt &goals_array = json_result.push_back_stream_array("goals");
96  for(const auto &property_pair : properties)
97  {
98  const property_infot &property_info = property_pair.second;
99 
100  json_objectt json_goal;
101  json_goal["status"] = json_stringt(
102  property_info.status == property_statust::FAIL ? "satisfied" : "failed");
103  json_goal["goal"] = json_stringt(property_pair.first);
104  json_goal["description"] = json_stringt(property_info.description);
105 
106  if(property_info.pc->source_location().is_not_nil())
107  json_goal["sourceLocation"] = json(property_info.pc->source_location());
108 
109  goals_array.push_back(std::move(json_goal));
110  }
111  const std::size_t goals_covered =
113  json_result.push_back(
114  "goalsCovered", json_numbert(std::to_string(goals_covered)));
115  json_result.push_back(
116  "totalGoals", json_numbert(std::to_string(properties.size())));
117 }
118 
120  const propertiest &properties,
121  unsigned iterations,
122  ui_message_handlert &ui_message_handler)
123 {
124  messaget log(ui_message_handler);
125  switch(ui_message_handler.get_ui())
126  {
128  {
129  output_goals_plain(properties, log);
130  break;
131  }
133  {
134  output_goals_xml(properties, log);
135  break;
136  }
138  {
139  output_goals_json(properties, log, ui_message_handler);
140  break;
141  }
142  }
143  output_goals_iterations(properties, iterations, log);
144 }
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.
source_locationt source_location
Definition: message.h:247
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
mstreamt & statistics() const
Definition: message.h:419
mstreamt & status() const
Definition: message.h:414
mstreamt & result() const
Definition: message.h:409
static eomt eom
Definition: message.h:297
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
xmlt & new_element(const std::string &key)
Definition: xml.h:95
static void output_goals_iterations(const propertiest &properties, unsigned iterations, messaget &log)
static void output_goals_xml(const propertiest &properties, messaget &log)
static void output_goals_json(const propertiest &properties, messaget &log, ui_message_handlert &ui_message_handler)
void output_goals(const propertiest &properties, unsigned iterations, ui_message_handlert &ui_message_handler)
Outputs the properties interpreted as 'coverage goals' and the number of goto verifier iterations tha...
static void output_goals_plain(const propertiest &properties, messaget &log)
Cover Goals Reporting Utilities.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:117
std::size_t count_properties(const propertiest &properties, property_statust status)
Return the number of properties with given status.
Definition: properties.cpp:160
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:108
@ FAIL
The property was violated.
std::map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition: properties.h:76
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
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