Skip to content

Commit b1587fa

Browse files
Utility for printing overall result
Enable consistent overall status reporting across all driver programs.
1 parent 02bc690 commit b1587fa

File tree

2 files changed

+25
-0
lines changed

2 files changed

+25
-0
lines changed

src/goto-checker/report_util.cpp

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -240,3 +240,24 @@ void output_properties(
240240
}
241241
}
242242
}
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: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,4 +25,8 @@ void output_properties(
2525
const propertiest &properties,
2626
ui_message_handlert &ui_message_handler);
2727

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

0 commit comments

Comments
 (0)