Skip to content

Commit 2c92ab1

Browse files
Utility for printing overall result
Enable consistent overall status reporting across all driver programs.
1 parent 0c898fa commit 2c92ab1

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
@@ -238,3 +238,24 @@ void output_properties(
238238
}
239239
}
240240
}
241+
242+
void output_overall_result(
243+
resultt result,
244+
ui_message_handlert &ui_message_handler)
245+
{
246+
switch(result)
247+
{
248+
case resultt::PASS:
249+
report_success(ui_message_handler);
250+
break;
251+
case resultt::FAIL:
252+
report_failure(ui_message_handler);
253+
break;
254+
case resultt::UNKNOWN:
255+
report_inconclusive(ui_message_handler);
256+
break;
257+
case resultt::ERROR:
258+
report_error(ui_message_handler);
259+
break;
260+
}
261+
}

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)