cprover
Loading...
Searching...
No Matches
properties.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Properties
4
5Author: Daniel Kroening, Peter Schrammel
6
7\*******************************************************************/
8
11
12#include "properties.h"
13
14#include <util/exit_codes.h>
15#include <util/invariant.h>
16#include <util/json.h>
17#include <util/json_stream.h>
18#include <util/xml.h>
19
21
22std::string as_string(resultt result)
23{
24 switch(result)
25 {
27 return "UNKNOWN";
28 case resultt::PASS:
29 return "PASS";
30 case resultt::FAIL:
31 return "FAIL";
32 case resultt::ERROR:
33 return "ERROR";
34 }
35
37}
38
39std::string as_string(property_statust status)
40{
41 switch(status)
42 {
44 return "NOT CHECKED";
46 return "UNKNOWN";
48 return "UNREACHABLE";
50 return "SUCCESS";
52 return "FAILURE";
54 return "ERROR";
55 }
56
58}
59
62 std::string description,
63 property_statust status)
64 : pc(pc), description(std::move(description)), status(status)
65{
66}
67
69{
70 propertiest properties;
71 update_properties_from_goto_model(properties, goto_model);
72 return properties;
73}
74
76 propertiest &properties,
77 const abstract_goto_modelt &goto_model)
78{
79 const auto &goto_functions = goto_model.get_goto_functions();
80 for(const auto &function_pair : goto_functions.function_map)
81 {
82 const goto_programt &goto_program = function_pair.second.body;
83
84 // need pointer to goto instruction
85 forall_goto_program_instructions(i_it, goto_program)
86 {
87 if(!i_it->is_assert())
88 continue;
89
90 std::string description =
91 id2string(i_it->source_location().get_comment());
92 if(description.empty())
93 description = "assertion";
94 properties.emplace(
95 i_it->source_location().get_property_id(),
96 property_infot{i_it, description, property_statust::NOT_CHECKED});
97 }
98 }
99}
100
101std::string
102as_string(const irep_idt &property_id, const property_infot &property_info)
103{
104 return "[" + id2string(property_id) + "] " + property_info.description +
105 ": " + as_string(property_info.status);
106}
107
108xmlt xml(const irep_idt &property_id, const property_infot &property_info)
109{
110 xmlt xml_result("result");
111 xml_result.set_attribute("property", id2string(property_id));
112 xml_result.set_attribute("status", as_string(property_info.status));
113 return xml_result;
114}
115
116template <class json_objectT>
117static void json(
118 json_objectT &result,
119 const irep_idt &property_id,
120 const property_infot &property_info)
121{
122 result["property"] = json_stringt(property_id);
123 result["description"] = json_stringt(property_info.description);
124 result["status"] = json_stringt(as_string(property_info.status));
125}
126
128json(const irep_idt &property_id, const property_infot &property_info)
129{
130 json_objectt result;
131 json<json_objectt>(result, property_id, property_info);
132 return result;
133}
134
135void json(
136 json_stream_objectt &result,
137 const irep_idt &property_id,
138 const property_infot &property_info)
139{
140 json<json_stream_objectt>(result, property_id, property_info);
141}
142
144{
145 switch(result)
146 {
147 case resultt::PASS:
149 case resultt::FAIL:
151 case resultt::ERROR:
153 case resultt::UNKNOWN:
155 }
157}
158
159std::size_t
161{
162 std::size_t count = 0;
163 for(const auto &property_pair : properties)
164 {
165 if(property_pair.second.status == status)
166 ++count;
167 }
168 return count;
169}
170
172{
173 return status == property_statust::NOT_CHECKED ||
175}
176
178{
179 for(const auto &property_pair : properties)
180 {
181 if(is_property_to_check(property_pair.second.status))
182 return true;
183 }
184 return false;
185}
186
194{
195 // non-monotonic use is likely a bug
196 // UNKNOWN is neutral element w.r.t. ERROR/PASS/NOT_REACHABLE/FAIL
197 // clang-format off
202 a == b);
203 // clang-format on
204 switch(a)
205 {
208 a = b;
209 return a;
214 return a;
215 }
217}
218
228{
229 switch(a)
230 {
232 return a;
234 a = (b == property_statust::ERROR ? b : a);
235 return a;
237 a = (b == property_statust::ERROR || b == property_statust::FAIL ? b : a);
238 return a;
240 a =
242 : a);
243 return a;
245 a = (b != property_statust::PASS ? b : a);
246 return a;
248 a = (b == property_statust::PASS ? a : b);
249 return a;
250 }
252}
253
261{
263 for(const auto &property_pair : properties)
264 {
265 status &= property_pair.second.status;
266 }
267 switch(status)
268 {
270 // If we have unchecked properties then we don't know.
271 return resultt::UNKNOWN;
273 return resultt::UNKNOWN;
275 // If a property is not reachable then overall it's still a PASS.
276 return resultt::PASS;
278 return resultt::PASS;
280 return resultt::FAIL;
282 return resultt::ERROR;
283 }
285}
Abstract interface to eager or lazy GOTO models.
Abstract interface to eager or lazy GOTO models.
virtual const goto_functionst & get_goto_functions() const =0
Accessor to get a raw goto_functionst.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst::const_iterator const_targett
Definition: goto_program.h:593
Provides methods for streaming JSON objects.
Definition: json_stream.h:140
Definition: xml.h:21
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:198
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
#define forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
STL namespace.
property_statust & operator&=(property_statust &a, property_statust const &b)
Update with the preference order.
Definition: properties.cpp:227
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:117
property_statust & operator|=(property_statust &a, property_statust const &b)
Update with the preference order.
Definition: properties.cpp:193
bool has_properties_to_check(const propertiest &properties)
Return true if there as a property with NOT_CHECKED or UNKNOWN status.
Definition: properties.cpp:177
bool is_property_to_check(property_statust status)
Return true if the status is NOT_CHECKED or UNKNOWN.
Definition: properties.cpp:171
resultt determine_result(const propertiest &properties)
Determines the overall result corresponding from the given properties That is PASS if all properties ...
Definition: properties.cpp:260
void update_properties_from_goto_model(propertiest &properties, const abstract_goto_modelt &goto_model)
Updates properties with the assertions in goto_model.
Definition: properties.cpp:75
std::size_t count_properties(const propertiest &properties, property_statust status)
Return the number of properties with given status.
Definition: properties.cpp:160
int result_to_exit_code(resultt result)
Definition: properties.cpp:143
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:108
std::string as_string(resultt result)
Definition: properties.cpp:22
propertiest initialize_properties(const abstract_goto_modelt &goto_model)
Returns the properties in the goto model.
Definition: properties.cpp:68
Properties.
property_statust
The status of a property.
Definition: properties.h:26
@ 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
A map of property IDs to property infos.
Definition: properties.h:76
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:503
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
property_statust status
The status of the property.
Definition: properties.h:72
std::string description
A description (usually derived from the assertion's comment)
Definition: properties.h:69
property_infot(goto_programt::const_targett pc, std::string description, property_statust status)
Definition: properties.cpp:60