cprover
Loading...
Searching...
No Matches
cover_goals_report_util.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Cover Goals Reporting Utilities
4
5Author: 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
41static 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
65static 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
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 & result() const
Definition: message.h:409
static eomt eom
Definition: message.h:297
mstreamt & status() const
Definition: message.h:414
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
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