cprover
properties.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Properties
4 
5 Author: Daniel Kroening, Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_CHECKER_PROPERTIES_H
13 #define CPROVER_GOTO_CHECKER_PROPERTIES_H
14 
15 #include <unordered_map>
16 
18 
19 class json_objectt;
21 class xmlt;
22 
24 enum class property_statust
25 {
29  UNKNOWN,
33  PASS,
35  FAIL,
37  ERROR
38 };
39 
40 std::string as_string(property_statust);
41 
43 enum class resultt
44 {
46  UNKNOWN,
48  PASS,
50  FAIL,
52  ERROR
53 };
54 
55 std::string as_string(resultt);
56 
58 {
61  std::string description,
63 
66 
68  std::string description;
69 
72 };
73 
75 typedef std::unordered_map<irep_idt, property_infot> propertiest;
76 
79 
82  propertiest &properties,
83  const abstract_goto_modelt &goto_model);
84 
85 std::string
86 as_string(const irep_idt &property_id, const property_infot &property_info);
87 
88 xmlt xml(const irep_idt &property_id, const property_infot &property_info);
89 
91 json(const irep_idt &property_id, const property_infot &property_info);
92 
94 void json(json_stream_objectt &, const irep_idt &, const property_infot &);
95 
96 int result_to_exit_code(resultt result);
97 
99 std::size_t count_properties(const propertiest &, property_statust);
100 
103 
105 bool has_properties_to_check(const propertiest &properties);
106 
109 resultt determine_result(const propertiest &properties);
110 
111 #endif // CPROVER_GOTO_CHECKER_PROPERTIES_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
propertiest
std::unordered_map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition: properties.h:75
property_statust::FAIL
@ FAIL
The property was violated.
property_statust
property_statust
The status of a property.
Definition: properties.h:25
property_statust::ERROR
@ ERROR
An error occurred during goto checking.
resultt
resultt
The result of goto verifying.
Definition: properties.h:44
operator&=
property_statust & operator&=(property_statust &, property_statust const &)
Update with the preference order.
Definition: properties.cpp:224
determine_result
resultt determine_result(const propertiest &properties)
Determines the overall result corresponding from the given properties That is PASS if all properties ...
Definition: properties.cpp:258
is_property_to_check
bool is_property_to_check(property_statust)
Return true if the status is NOT_CHECKED or UNKNOWN.
Definition: properties.cpp:168
goto_model.h
Symbol Table + CFG.
update_properties_from_goto_model
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:73
has_properties_to_check
bool has_properties_to_check(const propertiest &properties)
Return true if there as a property with NOT_CHECKED or UNKNOWN status.
Definition: properties.cpp:174
operator|=
property_statust & operator|=(property_statust &, property_statust const &)
Update with the preference order.
Definition: properties.cpp:190
resultt::UNKNOWN
@ UNKNOWN
No property was violated, neither was there an error.
property_statust::NOT_REACHABLE
@ NOT_REACHABLE
The property was proven to be unreachable.
property_infot::description
std::string description
A description (usually derived from the assertion's comment)
Definition: properties.h:68
json_objectt
Definition: json.h:300
result_to_exit_code
int result_to_exit_code(resultt result)
Definition: properties.cpp:140
property_infot::status
property_statust status
The status of the property.
Definition: properties.h:71
as_string
std::string as_string(property_statust)
Definition: properties.cpp:37
xml
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:105
count_properties
std::size_t count_properties(const propertiest &, property_statust)
Return the number of properties with given status.
Definition: properties.cpp:157
property_statust::NOT_CHECKED
@ NOT_CHECKED
The property was not checked (also used for initialization)
json
json_objectt json(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:125
xmlt
Definition: xml.h:21
resultt::ERROR
@ ERROR
An error occurred during goto checking.
property_statust::UNKNOWN
@ UNKNOWN
The checker was unable to determine the status of the property.
json_stream_objectt
Provides methods for streaming JSON objects.
Definition: json_stream.h:140
property_infot
Definition: properties.h:58
property_statust::PASS
@ PASS
The property was not violated.
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
initialize_properties
propertiest initialize_properties(const abstract_goto_modelt &)
Returns the properties in the goto model.
Definition: properties.cpp:66
abstract_goto_modelt
Abstract interface to eager or lazy GOTO models.
Definition: abstract_goto_model.h:21
property_infot::pc
goto_programt::const_targett pc
A pointer to the corresponding goto instruction.
Definition: properties.h:65
property_infot::property_infot
property_infot(goto_programt::const_targett pc, std::string description, property_statust status)
Definition: properties.cpp:58