Skip to content

Commit ce577d8

Browse files
tautschnigtautschnig
authored
Merge pull request #3584 from peterschrammel/overall-reporting-utils
Utilities for reporting overall result/status/exit code [depends: 3583, blocks: 3585]
2 parents dd52eec + b1587fa commit ce577d8

9 files changed

+164
-58
lines changed

‎src/cbmc/all_properties.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
1515
#include <chrono>
1616

1717
#include <goto-checker/bmc_util.h>
18+
#include <goto-checker/report_util.h>
1819

1920
#include <util/xml.h>
2021
#include <util/json.h>

‎src/cbmc/bmc.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,7 @@ Author: Daniel Kroening, [email protected]
2525
#include <linking/static_lifetime_init.h>
2626

2727
#include <goto-checker/bmc_util.h>
28+
#include <goto-checker/report_util.h>
2829
#include <goto-checker/solver_factory.h>
2930

3031
#include "counterexample_beautification.h"

‎src/cbmc/fault_localization.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,7 @@ Author: Peter Schrammel
2727
#include <goto-programs/xml_goto_trace.h>
2828

2929
#include <goto-checker/bmc_util.h>
30+
#include <goto-checker/report_util.h>
3031

3132
#include "counterexample_beautification.h"
3233

‎src/goto-checker/bmc_util.cpp

Lines changed: 0 additions & 55 deletions
Original file line numberDiff line numberDiff line change
@@ -225,58 +225,3 @@ void slice(
225225
<< " remaining after simplification" << messaget::eom;
226226
}
227227

228-
void report_success(ui_message_handlert &ui_message_handler)
229-
{
230-
messaget msg(ui_message_handler);
231-
msg.result() << "VERIFICATION SUCCESSFUL" << messaget::eom;
232-
233-
switch(ui_message_handler.get_ui())
234-
{
235-
case ui_message_handlert::uit::PLAIN:
236-
break;
237-
238-
case ui_message_handlert::uit::XML_UI:
239-
{
240-
xmlt xml("cprover-status");
241-
xml.data = "SUCCESS";
242-
msg.result() << xml;
243-
}
244-
break;
245-
246-
case ui_message_handlert::uit::JSON_UI:
247-
{
248-
json_objectt json_result;
249-
json_result["cProverStatus"] = json_stringt("success");
250-
msg.result() << json_result;
251-
}
252-
break;
253-
}
254-
}
255-
256-
void report_failure(ui_message_handlert &ui_message_handler)
257-
{
258-
messaget msg(ui_message_handler);
259-
msg.result() << "VERIFICATION FAILED" << messaget::eom;
260-
261-
switch(ui_message_handler.get_ui())
262-
{
263-
case ui_message_handlert::uit::PLAIN:
264-
break;
265-
266-
case ui_message_handlert::uit::XML_UI:
267-
{
268-
xmlt xml("cprover-status");
269-
xml.data = "FAILURE";
270-
msg.result() << xml;
271-
}
272-
break;
273-
274-
case ui_message_handlert::uit::JSON_UI:
275-
{
276-
json_objectt json_result;
277-
json_result["cProverStatus"] = json_stringt("failure");
278-
msg.result() << json_result;
279-
}
280-
break;
281-
}
282-
}

‎src/goto-checker/bmc_util.h

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -32,9 +32,6 @@ void convert_symex_target_equation(
3232
prop_convt &,
3333
message_handlert &);
3434

35-
void report_failure(ui_message_handlert &);
36-
void report_success(ui_message_handlert &);
37-
3835
void build_error_trace(
3936
goto_tracet &,
4037
const namespacet &,

‎src/goto-checker/properties.cpp

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ Author: Daniel Kroening, Peter Schrammel
1111

1212
#include "properties.h"
1313

14+
#include <util/exit_codes.h>
1415
#include <util/invariant.h>
1516
#include <util/json.h>
1617
#include <util/xml.h>
@@ -116,6 +117,22 @@ json(const irep_idt &property_id, const property_infot &property_info)
116117
return result;
117118
}
118119

120+
int result_to_exit_code(resultt result)
121+
{
122+
switch(result)
123+
{
124+
case resultt::PASS:
125+
return CPROVER_EXIT_VERIFICATION_SAFE;
126+
case resultt::FAIL:
127+
return CPROVER_EXIT_VERIFICATION_UNSAFE;
128+
case resultt::ERROR:
129+
return CPROVER_EXIT_INTERNAL_ERROR;
130+
case resultt::UNKNOWN:
131+
return CPROVER_EXIT_VERIFICATION_INCONCLUSIVE;
132+
}
133+
UNREACHABLE;
134+
}
135+
119136
std::size_t
120137
count_properties(const propertiest &properties, property_statust status)
121138
{

‎src/goto-checker/properties.h

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -84,6 +84,8 @@ xmlt xml(const irep_idt &property_id, const property_infot &property_info);
8484
json_objectt
8585
json(const irep_idt &property_id, const property_infot &property_info);
8686

87+
int result_to_exit_code(resultt result);
88+
8789
/// Return the number of properties with given \p status
8890
std::size_t count_properties(const propertiest &, property_statust);
8991

‎src/goto-checker/report_util.cpp

Lines changed: 133 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,118 @@ Author: Daniel Kroening, Peter Schrammel
1717
#include <util/ui_message.h>
1818
#include <util/xml.h>
1919

20+
void report_success(ui_message_handlert &ui_message_handler)
21+
{
22+
messaget msg(ui_message_handler);
23+
msg.result() << "VERIFICATION SUCCESSFUL" << messaget::eom;
24+
25+
switch(ui_message_handler.get_ui())
26+
{
27+
case ui_message_handlert::uit::PLAIN:
28+
break;
29+
30+
case ui_message_handlert::uit::XML_UI:
31+
{
32+
xmlt xml("cprover-status");
33+
xml.data = "SUCCESS";
34+
msg.result() << xml;
35+
}
36+
break;
37+
38+
case ui_message_handlert::uit::JSON_UI:
39+
{
40+
json_objectt json_result;
41+
json_result["cProverStatus"] = json_stringt("success");
42+
msg.result() << json_result;
43+
}
44+
break;
45+
}
46+
}
47+
48+
void report_failure(ui_message_handlert &ui_message_handler)
49+
{
50+
messaget msg(ui_message_handler);
51+
msg.result() << "VERIFICATION FAILED" << messaget::eom;
52+
53+
switch(ui_message_handler.get_ui())
54+
{
55+
case ui_message_handlert::uit::PLAIN:
56+
break;
57+
58+
case ui_message_handlert::uit::XML_UI:
59+
{
60+
xmlt xml("cprover-status");
61+
xml.data = "FAILURE";
62+
msg.result() << xml;
63+
}
64+
break;
65+
66+
case ui_message_handlert::uit::JSON_UI:
67+
{
68+
json_objectt json_result;
69+
json_result["cProverStatus"] = json_stringt("failure");
70+
msg.result() << json_result;
71+
}
72+
break;
73+
}
74+
}
75+
76+
void report_inconclusive(ui_message_handlert &ui_message_handler)
77+
{
78+
messaget msg(ui_message_handler);
79+
msg.result() << "VERIFICATION INCONCLUSIVE" << messaget::eom;
80+
81+
switch(ui_message_handler.get_ui())
82+
{
83+
case ui_message_handlert::uit::PLAIN:
84+
break;
85+
86+
case ui_message_handlert::uit::XML_UI:
87+
{
88+
xmlt xml("cprover-status");
89+
xml.data = "INCONCLUSIVE";
90+
msg.result() << xml;
91+
}
92+
break;
93+
94+
case ui_message_handlert::uit::JSON_UI:
95+
{
96+
json_objectt json_result;
97+
json_result["cProverStatus"] = json_stringt("inconclusive");
98+
msg.result() << json_result;
99+
}
100+
break;
101+
}
102+
}
103+
104+
void report_error(ui_message_handlert &ui_message_handler)
105+
{
106+
messaget msg(ui_message_handler);
107+
msg.result() << "VERIFICATION ERROR" << messaget::eom;
108+
109+
switch(ui_message_handler.get_ui())
110+
{
111+
case ui_message_handlert::uit::PLAIN:
112+
break;
113+
114+
case ui_message_handlert::uit::XML_UI:
115+
{
116+
xmlt xml("cprover-status");
117+
xml.data = "ERROR";
118+
msg.result() << xml;
119+
}
120+
break;
121+
122+
case ui_message_handlert::uit::JSON_UI:
123+
{
124+
json_objectt json_result;
125+
json_result["cProverStatus"] = json_stringt("error");
126+
msg.result() << json_result;
127+
}
128+
break;
129+
}
130+
}
131+
20132
void output_properties(
21133
const propertiest &properties,
22134
ui_message_handlert &ui_message_handler)
@@ -128,3 +240,24 @@ void output_properties(
128240
}
129241
}
130242
}
243+
244+
void output_overall_result(
245+
resultt result,
246+
ui_message_handlert &ui_message_handler)
247+
{
248+
switch(result)
249+
{
250+
case resultt::PASS:
251+
report_success(ui_message_handler);
252+
break;
253+
case resultt::FAIL:
254+
report_failure(ui_message_handler);
255+
break;
256+
case resultt::UNKNOWN:
257+
report_inconclusive(ui_message_handler);
258+
break;
259+
case resultt::ERROR:
260+
report_error(ui_message_handler);
261+
break;
262+
}
263+
}

‎src/goto-checker/report_util.h

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,8 +16,17 @@ Author: Daniel Kroening, Peter Schrammel
1616

1717
class ui_message_handlert;
1818

19+
void report_success(ui_message_handlert &);
20+
void report_failure(ui_message_handlert &);
21+
void report_inconclusive(ui_message_handlert &);
22+
void report_error(ui_message_handlert &);
23+
1924
void output_properties(
2025
const propertiest &properties,
2126
ui_message_handlert &ui_message_handler);
2227

28+
void output_overall_result(
29+
resultt result,
30+
ui_message_handlert &ui_message_handler);
31+
2332
#endif // CPROVER_GOTO_CHECKER_REPORT_UTIL_H

0 commit comments

Comments
 (0)