Add translation of final_result to CPROVER_EXIT_CODES

src/goto-bmc/goto_bmc_parse_options.cpp

@@ -8,6 +8,7 @@
 #include <goto-programs/read_goto_binary.h>
 
 #include <libcprover-cpp/api_options.h>
+#include <libcprover-cpp/verification_result.h>
 
 #include "api.h"
 
@@ -78,7 +79,7 @@ int core_cbmc_only_parse_optionst::doit()
   // ... and run analysis on it.
   auto result = api.run_verifier();
 
-  return CPROVER_EXIT_SUCCESS;
+  return verifier_result_to_exit_code(result->final_result());
 }
 
 void core_cbmc_only_parse_optionst::help()

src/libcprover-cpp/verification_result.cpp

@@ -6,6 +6,7 @@
 
 #include "verification_result.h"
 
+#include <util/exit_codes.h>
 #include <util/invariant.h>
 #include <util/make_unique.h>
 
@@ -149,3 +150,20 @@ verification_resultt::get_property_status(const std::string &property_id) const
   }
   UNREACHABLE;
 }
+
+// FOTIS' note: Modelled after `result_to_exit_code` in `src/goto-checker/properties.cpp`
+int verifier_result_to_exit_code(verifier_resultt result)
+{
+  switch(result)
+  {
+  case verifier_resultt::PASS:
+    return CPROVER_EXIT_VERIFICATION_SAFE;
+  case verifier_resultt::FAIL:
+    return CPROVER_EXIT_VERIFICATION_UNSAFE;
+  case verifier_resultt::ERROR:
+    return CPROVER_EXIT_INTERNAL_ERROR;
+  case verifier_resultt::UNKNOWN:
+    return CPROVER_EXIT_VERIFICATION_INCONCLUSIVE;
+  }
+  UNREACHABLE;
+}

src/libcprover-cpp/verification_result.h

@@ -80,4 +80,8 @@ struct verification_resultt
   std::unique_ptr<verification_result_implt> _impl;
 };
 
+// Allow translation of `verifier_resultt` into a CPROVER_EXIT_CODES (so that
+// they can be consistent across various tools using the API).
+int verifier_result_to_exit_code(verifier_resultt result);
+
 #endif // CPROVER_GOTO_CHECKER_VERIFICATION_RESULT_H