47 _verifier_result = result;
52 return _verifier_result;
88 _impl->set_properties(properties);
93 _impl->set_result(result);
98 switch(
_impl->get_result())
115 std::vector<std::string> result;
116 for(
const auto &props :
_impl->get_properties())
118 result.push_back(
as_string(props.first));
124 const std::string &property_id)
const
126 auto irepidt_property =
irep_idt(property_id);
127 const auto description =
128 _impl->get_properties().at(irepidt_property).description;
135 auto irepidt_property =
irep_idt(property_id);
136 switch(
_impl->get_properties().at(irepidt_property).status)
const propertiest & get_properties()
verification_result_implt(const verification_result_implt &other)=default
void set_properties(propertiest &properties)
verification_result_implt()=default
~verification_result_implt()=default
void set_result(resultt &verification_result)
Document and give macros for the exit codes of CPROVER binaries.
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
#define CPROVER_EXIT_VERIFICATION_SAFE
Verification successful indicates the analysis has been performed without error AND the software is s...
#define CPROVER_EXIT_VERIFICATION_INCONCLUSIVE
Verification inconclusive indicates the analysis has been performed without error AND the software is...
#define CPROVER_EXIT_VERIFICATION_UNSAFE
Verification successful indicates the analysis has been performed without error AND the software is n...
std::unique_ptr< T > util_make_unique(Ts &&... ts)
@ UNKNOWN
The checker was unable to determine the status of the property.
@ NOT_REACHABLE
The property was proven to be unreachable.
@ PASS
The property was not violated.
@ ERROR
An error occurred during goto checking.
@ FAIL
The property was violated.
@ NOT_CHECKED
The property was not checked (also used for initialization)
resultt
The result of goto verifying.
@ UNKNOWN
No property was violated, neither was there an error.
@ PASS
No properties were violated.
@ ERROR
An error occurred during goto checking.
@ FAIL
Some properties were violated.
#define UNREACHABLE
This should be used to mark dead code.
std::string as_string(const ai_verifier_statust &status)
Makes a status message string from a status.
verification_resultt & operator=(verification_resultt &&)
std::vector< std::string > get_property_ids() const
void set_result(resultt &result)
std::unique_ptr< verification_result_implt > _impl
std::string get_property_description(const std::string &property_id) const
void set_properties(propertiest &properties)
prop_statust get_property_status(const std::string &property_id) const
verifier_resultt final_result() const
int verifier_result_to_exit_code(verifier_resultt result)
Interface for the various verification engines providing results.
@ PASS
No properties were violated.
@ ERROR
An error occurred during goto checking.
@ FAIL
Some properties were violated.
@ UNKNOWN
The checker was unable to determine the status of the property.
@ NOT_REACHABLE
The property was proven to be unreachable.
@ PASS
The property was not violated.
@ ERROR
An error occurred during goto checking.
@ FAIL
The property was violated.
@ NOT_CHECKED
The property was not checked (also used for initialization)
std::map< irep_idt, property_infot > propertiest