Skip to content

Commit a312377

Browse files
peterschrammelpeterschrammel
committed
Add report_util for outputting verification results
Prints the property report in plain text, JSON or XML.
1 parent 704505d commit a312377

File tree

3 files changed

+151
-0
lines changed

3 files changed

+151
-0
lines changed

‎src/goto-checker/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@ SRC = bmc_util.cpp \
22
incremental_goto_checker.cpp \
33
goto_verifier.cpp \
44
properties.cpp \
5+
report_util.cpp \
56
solver_factory.cpp \
67
symex_coverage.cpp \
78
symex_bmc.cpp \

‎src/goto-checker/report_util.cpp

Lines changed: 127 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,127 @@
1+
/*******************************************************************\
2+
3+
Module: Bounded Model Checking Utilities
4+
5+
Author: Daniel Kroening, Peter Schrammel
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Bounded Model Checking Utilities
11+
12+
#include "report_util.h"
13+
14+
#include <util/ui_message.h>
15+
#include <util/xml.h>
16+
17+
void output_properties(
18+
const propertiest &properties,
19+
ui_message_handlert &ui_message_handler)
20+
{
21+
messaget log(ui_message_handler);
22+
switch(ui_message_handler.get_ui())
23+
{
24+
case ui_message_handlert::uit::PLAIN:
25+
{
26+
log.result() << "\n** Results:" << messaget::eom;
27+
// collect properties in a vector
28+
std::vector<propertiest::const_iterator> sorted_properties;
29+
for(auto p_it = properties.begin(); p_it != properties.end(); p_it++)
30+
sorted_properties.push_back(p_it);
31+
// now determine an ordering for those goals:
32+
// 1. alphabetical ordering of file name
33+
// 2. numerical ordering of line number
34+
// 3. alphabetical ordering of goal ID
35+
std::sort(
36+
sorted_properties.begin(),
37+
sorted_properties.end(),
38+
[](propertiest::const_iterator pit1, propertiest::const_iterator pit2) {
39+
const auto &p1 = pit1->second.pc->source_location;
40+
const auto &p2 = pit2->second.pc->source_location;
41+
if(p1.get_file() != p2.get_file())
42+
return id2string(p1.get_file()) < id2string(p2.get_file());
43+
else if(!p1.get_line().empty() && !p2.get_line().empty())
44+
return std::stoul(id2string(p1.get_line())) <
45+
std::stoul(id2string(p2.get_line()));
46+
else
47+
return id2string(pit1->first) < id2string(pit2->first);
48+
});
49+
// now show in the order we have determined
50+
irep_idt previous_function;
51+
irep_idt current_file;
52+
for(const auto &p : sorted_properties)
53+
{
54+
const auto &l = p->second.pc->source_location;
55+
if(l.get_function() != previous_function)
56+
{
57+
if(!previous_function.empty())
58+
log.result() << '\n';
59+
previous_function = l.get_function();
60+
if(!previous_function.empty())
61+
{
62+
current_file = l.get_file();
63+
if(!current_file.empty())
64+
log.result() << current_file << ' ';
65+
if(!l.get_function().empty())
66+
log.result() << "function " << l.get_function();
67+
log.result() << messaget::eom;
68+
}
69+
}
70+
log.result() << messaget::faint << '[' << p->first << "] "
71+
<< messaget::reset;
72+
if(l.get_file() != current_file)
73+
log.result() << "file " << l.get_file() << ' ';
74+
if(!l.get_line().empty())
75+
log.result() << "line " << l.get_line() << ' ';
76+
log.result() << p->second.description << ": ";
77+
switch(p->second.status)
78+
{
79+
case property_statust::NOT_CHECKED:
80+
log.result() << messaget::magenta;
81+
break;
82+
case property_statust::UNKNOWN:
83+
log.result() << messaget::yellow;
84+
break;
85+
case property_statust::NOT_REACHABLE:
86+
log.result() << messaget::bright_green;
87+
break;
88+
case property_statust::PASS:
89+
log.result() << messaget::green;
90+
break;
91+
case property_statust::FAIL:
92+
log.result() << messaget::red;
93+
break;
94+
case property_statust::ERROR:
95+
log.result() << messaget::bright_red;
96+
break;
97+
}
98+
log.result() << as_string(p->second.status) << messaget::reset
99+
<< messaget::eom;
100+
}
101+
log.status() << "\n** "
102+
<< count_properties(properties, property_statust::FAIL)
103+
<< " of " << properties.size() << " failed" << messaget::eom;
104+
break;
105+
}
106+
case ui_message_handlert::uit::XML_UI:
107+
{
108+
for(const auto &property_pair : properties)
109+
{
110+
log.result() << xml(property_pair.first, property_pair.second);
111+
}
112+
break;
113+
}
114+
case ui_message_handlert::uit::JSON_UI:
115+
{
116+
json_stream_objectt &json_result =
117+
ui_message_handler.get_json_stream().push_back_stream_object();
118+
json_stream_arrayt &result_array =
119+
json_result.push_back_stream_array("result");
120+
for(const auto &property_pair : properties)
121+
{
122+
result_array.push_back(json(property_pair.first, property_pair.second));
123+
}
124+
break;
125+
}
126+
}
127+
}

‎src/goto-checker/report_util.h

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
/*******************************************************************\
2+
3+
Module: Bounded Model Checking Utilities
4+
5+
Author: Daniel Kroening, Peter Schrammel
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Bounded Model Checking Utilities
11+
12+
#ifndef CPROVER_GOTO_CHECKER_REPORT_UTIL_H
13+
#define CPROVER_GOTO_CHECKER_REPORT_UTIL_H
14+
15+
#include "properties.h"
16+
17+
class ui_message_handlert;
18+
19+
void output_properties(
20+
const propertiest &properties,
21+
ui_message_handlert &ui_message_handler);
22+
23+
#endif // CPROVER_GOTO_CHECKER_REPORT_UTIL_H

0 commit comments

Comments
 (0)