Skip to content

Commit 0c898fa

Browse files
Add result_to_exit_code
Enable consistent result-dependent exit codes across all driver programs.
1 parent b15033e commit 0c898fa

File tree

2 files changed

+18
-0
lines changed

2 files changed

+18
-0
lines changed

src/goto-checker/properties.cpp

Lines changed: 16 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>
@@ -106,6 +107,21 @@ json(const irep_idt &property_id, const property_infot &property_info)
106107
return result;
107108
}
108109

110+
int result_to_exit_code(resultt result)
111+
{
112+
switch(result)
113+
{
114+
case resultt::PASS:
115+
return CPROVER_EXIT_VERIFICATION_SAFE;
116+
case resultt::FAIL:
117+
return CPROVER_EXIT_VERIFICATION_UNSAFE;
118+
case resultt::ERROR:
119+
return CPROVER_EXIT_INTERNAL_ERROR;
120+
case resultt::UNKNOWN:
121+
return CPROVER_EXIT_VERIFICATION_INCONCLUSIVE;
122+
}
123+
}
124+
109125
/// Returns the number of properties with given \p result
110126
std::size_t
111127
count_properties(const propertiest &properties, property_resultt result)

src/goto-checker/properties.h

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -79,6 +79,8 @@ xmlt xml(const irep_idt &property_id, const property_infot &property_info);
7979
json_objectt
8080
json(const irep_idt &property_id, const property_infot &property_info);
8181

82+
int result_to_exit_code(resultt result);
83+
8284
std::size_t
8385
count_properties(const propertiest &properties, property_resultt result);
8486

0 commit comments

Comments
 (0)