diff --git a/src/goto-bmc/goto_bmc_parse_options.cpp b/src/goto-bmc/goto_bmc_parse_options.cpp index 474232d6c79f..cfa80aa0d3d4 100644 --- a/src/goto-bmc/goto_bmc_parse_options.cpp +++ b/src/goto-bmc/goto_bmc_parse_options.cpp @@ -8,6 +8,7 @@ #include #include +#include #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() diff --git a/src/libcprover-cpp/verification_result.cpp b/src/libcprover-cpp/verification_result.cpp index 25f81df7e480..04fc46fe0caa 100644 --- a/src/libcprover-cpp/verification_result.cpp +++ b/src/libcprover-cpp/verification_result.cpp @@ -6,6 +6,7 @@ #include "verification_result.h" +#include #include #include @@ -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; +} diff --git a/src/libcprover-cpp/verification_result.h b/src/libcprover-cpp/verification_result.h index b8525edac054..778299315168 100644 --- a/src/libcprover-cpp/verification_result.h +++ b/src/libcprover-cpp/verification_result.h @@ -80,4 +80,8 @@ struct verification_resultt std::unique_ptr _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