cprover
Loading...
Searching...
No Matches
verification_result.cpp
Go to the documentation of this file.
1// Copyright (c) 2023 Fotis Koutoulakis for Diffblue Ltd.
2
5// in a structured form.
6
8
9#include <util/exit_codes.h>
10#include <util/invariant.h>
11#include <util/make_unique.h>
12
14
15#include <algorithm>
16#include <string>
17#include <vector>
18
35
36// Impl
37
43
45 resultt &result)
46{
47 _verifier_result = result;
48}
49
54
55const propertiest &
60
61// Verification_result
62
67
71
76
81{
82 *_impl = *other._impl;
83 return *this;
84}
85
87{
88 _impl->set_properties(properties);
89}
90
92{
93 _impl->set_result(result);
94}
95
97{
98 switch(_impl->get_result())
99 {
100 case resultt::ERROR:
102 case resultt::FAIL:
104 case resultt::PASS:
106 case resultt::UNKNOWN:
108 }
109 // Required to silence compiler warnings that are promoted as errors!
111}
112
113std::vector<std::string> verification_resultt::get_property_ids() const
114{
115 std::vector<std::string> result;
116 for(const auto &props : _impl->get_properties())
117 {
118 result.push_back(as_string(props.first));
119 }
120 return result;
121}
122
124 const std::string &property_id) const
125{
126 auto irepidt_property = irep_idt(property_id);
127 const auto description =
128 _impl->get_properties().at(irepidt_property).description;
129 return description;
130}
131
133verification_resultt::get_property_status(const std::string &property_id) const
134{
135 auto irepidt_property = irep_idt(property_id);
136 switch(_impl->get_properties().at(irepidt_property).status)
137 {
139 return prop_statust::ERROR;
141 return prop_statust::FAIL;
147 return prop_statust::PASS;
150 }
152}
153
154// FOTIS' note: Modelled after `result_to_exit_code` in
155// `src/goto-checker/properties.cpp`.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
verification_result_implt(const verification_result_implt &other)=default
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.
Definition exit_codes.h:45
#define CPROVER_EXIT_VERIFICATION_SAFE
Verification successful indicates the analysis has been performed without error AND the software is s...
Definition exit_codes.h:21
#define CPROVER_EXIT_VERIFICATION_INCONCLUSIVE
Verification inconclusive indicates the analysis has been performed without error AND the software is...
Definition exit_codes.h:30
#define CPROVER_EXIT_VERIFICATION_UNSAFE
Verification successful indicates the analysis has been performed without error AND the software is n...
Definition exit_codes.h:25
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition make_unique.h:19
Properties.
@ 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.
Definition properties.h:45
@ 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.
Definition invariant.h:525
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.
dstringt irep_idt
verifier_resultt
@ 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