Add result_to_exit_code

Enable consistent result-dependent exit codes across all
driver programs.

Author: peterschrammel

src/goto-checker/properties.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include "properties.h"
 
+#include <util/exit_codes.h>
 #include <util/invariant.h>
 #include <util/json.h>
 #include <util/xml.h>
@@ -116,6 +117,22 @@ json(const irep_idt &property_id, const property_infot &property_info)
   return result;
 }
 
+int result_to_exit_code(resultt result)
+{
+  switch(result)
+  {
+  case resultt::PASS:
+    return CPROVER_EXIT_VERIFICATION_SAFE;
+  case resultt::FAIL:
+    return CPROVER_EXIT_VERIFICATION_UNSAFE;
+  case resultt::ERROR:
+    return CPROVER_EXIT_INTERNAL_ERROR;
+  case resultt::UNKNOWN:
+    return CPROVER_EXIT_VERIFICATION_INCONCLUSIVE;
+  }
+  UNREACHABLE;
+}
+
 std::size_t
 count_properties(const propertiest &properties, property_statust status)
 {

src/goto-checker/properties.h

@@ -84,6 +84,8 @@ xmlt xml(const irep_idt &property_id, const property_infot &property_info);
 json_objectt
 json(const irep_idt &property_id, const property_infot &property_info);
 
+int result_to_exit_code(resultt result);
+
 /// Return the number of properties with given \p status
 std::size_t count_properties(const propertiest &, property_statust);