CBMC
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_irep.h>
18#include <util/json_stream.h>
19#include <util/xml.h>
20#include <util/xml_irep.h>
21
23
24std::string as_string(resultt result)
25{
26 switch(result)
27 {
29 return "UNKNOWN";
30 case resultt::PASS:
31 return "PASS";
32 case resultt::FAIL:
33 return "FAIL";
34 case resultt::ERROR:
35 return "ERROR";
36 }
37
39}
40
41std::string as_string(property_statust status)
42{
43 switch(status)
44 {
46 return "NOT CHECKED";
48 return "UNKNOWN";
50 return "UNREACHABLE";
52 return "SUCCESS";
54 return "FAILURE";
56 return "ERROR";
57 }
58
60}
61
64 std::string description,
65 property_statust status)
66 : pc(pc), description(std::move(description)), status(status)
67{
68}
69
71{
72 propertiest properties;
73 update_properties_from_goto_model(properties, goto_model);
74 return properties;
75}
76
78 propertiest &properties,
79 const abstract_goto_modelt &goto_model)
80{
81 const auto &goto_functions = goto_model.get_goto_functions();
82 for(const auto &function_pair : goto_functions.function_map)
83 {
84 const goto_programt &goto_program = function_pair.second.body;
85
86 // need pointer to goto instruction
88 {
89 if(!i_it->is_assert())
90 continue;
91
92 std::string description =
93 id2string(i_it->source_location().get_comment());
94 if(description.empty())
95 description = "assertion";
96 properties.emplace(
97 i_it->source_location().get_property_id(),
98 property_infot{i_it, description, property_statust::NOT_CHECKED});
99 }
100 }
101}
102
103std::string
105{
106 return "[" + id2string(property_id) + "] " + property_info.description +
107 ": " + as_string(property_info.status);
108}
109
110xmlt xml(const irep_idt &property_id, const property_infot &property_info)
111{
112 xmlt xml_result("result");
113 xml_result.set_attribute("property", id2string(property_id));
114 xml_result.set_attribute("status", as_string(property_info.status));
115 xml_result.new_element(xml(property_info.pc->source_location()));
116 return xml_result;
117}
118
119template <class json_objectT>
120static void json(
121 json_objectT &result,
122 const irep_idt &property_id,
124{
125 result["property"] = json_stringt(property_id);
126 result["description"] = json_stringt(property_info.description);
127 result["status"] = json_stringt(as_string(property_info.status));
128 result["sourceLocation"] = json(property_info.pc->source_location());
129}
130
132json(const irep_idt &property_id, const property_infot &property_info)
133{
134 json_objectt result;
135 json<json_objectt>(result, property_id, property_info);
136 return result;
137}
138
139void json(
140 json_stream_objectt &result,
141 const irep_idt &property_id,
143{
144 json<json_stream_objectt>(result, property_id, property_info);
145}
146
148{
149 switch(result)
150 {
151 case resultt::PASS:
153 case resultt::FAIL:
155 case resultt::ERROR:
157 case resultt::UNKNOWN:
159 }
161}
162
163std::size_t
165{
166 std::size_t count = 0;
167 for(const auto &property_pair : properties)
168 {
169 if(property_pair.second.status == status)
170 ++count;
171 }
172 return count;
173}
174
176{
177 return status == property_statust::NOT_CHECKED ||
179}
180
182{
183 for(const auto &property_pair : properties)
184 {
185 if(is_property_to_check(property_pair.second.status))
186 return true;
187 }
188 return false;
189}
190
198{
199 // non-monotonic use is likely a bug
200 // UNKNOWN is neutral element w.r.t. ERROR/PASS/NOT_REACHABLE/FAIL
201 // clang-format off
206 a == b);
207 // clang-format on
208 switch(a)
209 {
212 a = b;
213 return a;
218 return a;
219 }
221}
222
232{
233 switch(a)
234 {
236 return a;
238 a = (b == property_statust::ERROR ? b : a);
239 return a;
242 return a;
244 a =
246 : a);
247 return a;
249 a = (b != property_statust::PASS ? b : a);
250 return a;
252 a = (b == property_statust::PASS ? a : b);
253 return a;
254 }
256}
257
265{
267 for(const auto &property_pair : properties)
268 {
269 status &= property_pair.second.status;
270 }
271 switch(status)
272 {
274 // If we have unchecked properties then we don't know.
275 return resultt::UNKNOWN;
277 return resultt::UNKNOWN;
279 // If a property is not reachable then overall it's still a PASS.
280 return resultt::PASS;
282 return resultt::PASS;
284 return resultt::FAIL;
286 return resultt::ERROR;
287 }
289}
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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
Provides methods for streaming JSON objects.
Definition xml.h:21
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:44
STL namespace.
property_statust & operator&=(property_statust &a, property_statust const &b)
Update with the preference order.
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
property_statust & operator|=(property_statust &a, property_statust const &b)
Update with the preference order.
bool has_properties_to_check(const propertiest &properties)
Return true if there as a property with NOT_CHECKED or UNKNOWN status.
bool is_property_to_check(property_statust status)
Return true if the status is NOT_CHECKED or UNKNOWN.
resultt determine_result(const propertiest &properties)
Determines the overall result corresponding from the given properties That is PASS if all properties ...
void update_properties_from_goto_model(propertiest &properties, const abstract_goto_modelt &goto_model)
Updates properties with the assertions in goto_model.
std::size_t count_properties(const propertiest &properties, property_statust status)
Return the number of properties with given status.
int result_to_exit_code(resultt result)
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
std::string as_string(resultt result)
propertiest initialize_properties(const abstract_goto_modelt &goto_model)
Returns the properties in the goto model.
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:525
#define PRECONDITION(CONDITION)
Definition invariant.h:463
property_infot(goto_programt::const_targett pc, std::string description, property_statust status)