cprover
Loading...
Searching...
No Matches
verification_result.h
Go to the documentation of this file.
1// Copyright (c) 2023 Fotis Koutoulakis for Diffblue Ltd.
2
5// in a structured form.
6
7#ifndef CPROVER_LIBCPROVER_CPP_VERIFICATION_RESULT_H
8#define CPROVER_LIBCPROVER_CPP_VERIFICATION_RESULT_H
9
10#include <map>
11#include <memory>
12#include <string>
13#include <vector>
14
15#ifndef USE_STD_STRING
16# define USE_DSTRING
17#endif
18
19#ifdef USE_DSTRING
20class dstringt;
22#else
23typedef std::string irep_idt;
24#endif
25
26struct property_infot;
27using propertiest = std::map<irep_idt, property_infot>;
28enum class resultt;
29
30// The enumerations here mirror the ones in properties.h.
31// The reason we do so is that we want to expose the same information
32// to users of the API, without including (and therefore, exposing)
33// CBMC internal headers.
34
35enum class prop_statust
36{
40 UNKNOWN,
44 PASS,
46 FAIL,
48 ERROR
49};
50
52{
53 UNKNOWN,
55 PASS,
57 FAIL,
59 ERROR
60};
61
63{
69
70 void set_result(resultt &result);
71 void set_properties(propertiest &properties);
72
74 std::vector<std::string> get_property_ids() const;
75 std::string get_property_description(const std::string &property_id) const;
76 prop_statust get_property_status(const std::string &property_id) const;
77
78private:
80 std::unique_ptr<verification_result_implt> _impl;
81};
82
83// Allow translation of `verifier_resultt` into a CPROVER_EXIT_CODES (so that
84// they can be consistent across various tools using the API).
86
87#endif // CPROVER_GOTO_CHECKER_VERIFICATION_RESULT_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
std::map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition properties.h:76
resultt
The result of goto verifying.
Definition properties.h:45
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
dstringt irep_idt
verifier_resultt
@ 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
int verifier_result_to_exit_code(verifier_resultt result)