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/ui_message.h>
19 #include <util/xml.h>
20 #include <util/xml_irep.h>
21 
23  const propertiest &properties,
24  unsigned iterations,
25  messaget &log)
26 {
27  const std::size_t goals_covered =
29  log.status() << "** " << goals_covered << " of " << properties.size()
30  << " covered (" << std::fixed << std::setw(1)
31  << std::setprecision(1)
32  << (properties.empty()
33  ? 100.0
34  : 100.0 * goals_covered / properties.size())
35  << "%)" << messaget::eom;
36  log.statistics() << "** Used " << iterations << " iteration"
37  << (iterations == 1 ? "" : "s") << messaget::eom;
38 }
39 
40 static void output_goals_plain(const propertiest &properties, messaget &log)
41 {
42  log.result() << "\n** coverage results:" << messaget::eom;
43 
44  for(const auto &property_pair : properties)
45  {
46  log.result() << "[" << property_pair.first << "]";
47 
48  if(property_pair.second.pc->source_location.is_not_nil())
49  log.result() << ' ' << property_pair.second.pc->source_location;
50 
51  if(!property_pair.second.description.empty())
52  log.result() << ' ' << property_pair.second.description;
53 
54  log.result() << ": "
55  << (property_pair.second.status == property_statust::FAIL
56  ? "SATISFIED"
57  : "FAILED")
58  << '\n';
59  }
60 
61  log.result() << messaget::eom;
62 }
63 
64 static void output_goals_xml(const propertiest &properties, messaget &log)
65 {
66  for(const auto &property_pair : properties)
67  {
68  xmlt xml_result(
69  "goal",
70  {{"id", id2string(property_pair.first)},
71  {"description", property_pair.second.description},
72  {"status",
73  property_pair.second.status == property_statust::FAIL ? "SATISFIED"
74  : "FAILED"}},
75  {});
76 
77  if(property_pair.second.pc->source_location.is_not_nil())
78  xml_result.new_element() = xml(property_pair.second.pc->source_location);
79 
80  log.result() << xml_result;
81  }
82 }
83 
84 static void output_goals_json(
85  const propertiest &properties,
86  messaget &log,
87  ui_message_handlert &ui_message_handler)
88 {
89  if(log.status().tellp() > 0)
90  log.status() << messaget::eom; // force end of previous message
91  json_stream_objectt &json_result =
92  ui_message_handler.get_json_stream().push_back_stream_object();
93  json_stream_arrayt &goals_array = json_result.push_back_stream_array("goals");
94  for(const auto &property_pair : properties)
95  {
96  const property_infot &property_info = property_pair.second;
97 
98  json_objectt json_goal;
99  json_goal["status"] = json_stringt(
100  property_info.status == property_statust::FAIL ? "satisfied" : "failed");
101  json_goal["goal"] = json_stringt(property_pair.first);
102  json_goal["description"] = json_stringt(property_info.description);
103 
104  if(property_info.pc->source_location.is_not_nil())
105  json_goal["sourceLocation"] = json(property_info.pc->source_location);
106 
107  goals_array.push_back(std::move(json_goal));
108  }
109  const std::size_t goals_covered =
111  json_result.push_back(
112  "goalsCovered", json_numbert(std::to_string(goals_covered)));
113  json_result.push_back(
114  "totalGoals", json_numbert(std::to_string(properties.size())));
115 }
116 
118  const propertiest &properties,
119  unsigned iterations,
120  ui_message_handlert &ui_message_handler)
121 {
122  messaget log(ui_message_handler);
123  switch(ui_message_handler.get_ui())
124  {
126  {
127  output_goals_plain(properties, log);
128  break;
129  }
131  {
132  output_goals_xml(properties, log);
133  break;
134  }
136  {
137  output_goals_json(properties, log, ui_message_handler);
138  break;
139  }
140  }
141  output_goals_iterations(properties, iterations, log);
142 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
propertiest
std::unordered_map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition: properties.h:75
json_numbert
Definition: json.h:291
property_statust::FAIL
@ FAIL
The property was violated.
ui_message_handlert
Definition: ui_message.h:20
ui_message_handlert::uit::XML_UI
@ XML_UI
messaget::status
mstreamt & status() const
Definition: message.h:414
output_goals_json
static void output_goals_json(const propertiest &properties, messaget &log, ui_message_handlert &ui_message_handler)
Definition: cover_goals_report_util.cpp:84
output_goals_iterations
static void output_goals_iterations(const propertiest &properties, unsigned iterations, messaget &log)
Definition: cover_goals_report_util.cpp:22
xml_irep.h
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
output_goals_xml
static void output_goals_xml(const propertiest &properties, messaget &log)
Definition: cover_goals_report_util.cpp:64
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
output_goals
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...
Definition: cover_goals_report_util.cpp:117
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
ui_message_handlert::get_json_stream
virtual json_stream_arrayt & get_json_stream()
Definition: ui_message.h:38
property_infot::status
property_statust status
The status of the property.
Definition: properties.h:71
cover_goals_report_util.h
Cover Goals Reporting Utilities.
messaget::result
mstreamt & result() const
Definition: message.h:409
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
xml
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:105
ui_message_handlert::uit::JSON_UI
@ JSON_UI
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:247
json
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:114
json_stream_arrayt
Provides methods for streaming JSON arrays.
Definition: json_stream.h:93
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
xmlt
Definition: xml.h:21
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
json_stream_objectt
Provides methods for streaming JSON objects.
Definition: json_stream.h:140
property_infot
Definition: properties.h:58
ui_message_handlert::uit::PLAIN
@ PLAIN
json.h
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
output_goals_plain
static void output_goals_plain(const propertiest &properties, messaget &log)
Definition: cover_goals_report_util.cpp:40
property_infot::pc
goto_programt::const_targett pc
A pointer to the corresponding goto instruction.
Definition: properties.h:65
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
xmlt::new_element
xmlt & new_element(const std::string &key)
Definition: xml.h:95
messaget::statistics
mstreamt & statistics() const
Definition: message.h:419
json_stringt
Definition: json.h:270
ui_message.h