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 
20 class json_objectt;
22 class xmlt;
23 
25 enum class property_statust
26 {
28  NOT_CHECKED,
30  UNKNOWN,
32  NOT_REACHABLE,
34  PASS,
36  FAIL,
38  ERROR
39 };
40 
41 std::string as_string(property_statust);
42 
44 enum class resultt
45 {
47  UNKNOWN,
49  PASS,
51  FAIL,
53  ERROR
54 };
55 
56 std::string as_string(resultt);
57 
59 {
62  std::string description,
64 
67 
69  std::string description;
70 
73 };
74 
76 typedef std::unordered_map<irep_idt, property_infot> propertiest;
77 
80 
83  propertiest &properties,
84  const abstract_goto_modelt &goto_model);
85 
86 std::string
87 as_string(const irep_idt &property_id, const property_infot &property_info);
88 
89 xmlt xml(const irep_idt &property_id, const property_infot &property_info);
90 
92 json(const irep_idt &property_id, const property_infot &property_info);
93 
95 void json(json_stream_objectt &, const irep_idt &, const property_infot &);
96 
97 int result_to_exit_code(resultt result);
98 
100 std::size_t count_properties(const propertiest &, property_statust);
101 
104 
106 bool has_properties_to_check(const propertiest &properties);
107 
110 resultt determine_result(const propertiest &properties);
111 
112 #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:76
property_statust
property_statust
The status of a property.
Definition: properties.h:26
property_statust::ERROR
@ ERROR
An error occurred during goto checking.
resultt
resultt
The result of goto verifying.
Definition: properties.h:45
operator&=
property_statust & operator&=(property_statust &, property_statust const &)
Update with the preference order.
Definition: properties.cpp:226
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:259
is_property_to_check
bool is_property_to_check(property_statust)
Return true if the status is NOT_CHECKED or UNKNOWN.
Definition: properties.cpp:170
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:75
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:176
operator|=
property_statust & operator|=(property_statust &, property_statust const &)
Update with the preference order.
Definition: properties.cpp:192
resultt::UNKNOWN
@ UNKNOWN
No property was violated, neither was there an error.
property_infot::description
std::string description
A description (usually derived from the assertion's comment)
Definition: properties.h:69
json_objectt
Definition: json.h:300
result_to_exit_code
int result_to_exit_code(resultt result)
Definition: properties.cpp:142
property_infot::status
property_statust status
The status of the property.
Definition: properties.h:72
as_string
std::string as_string(property_statust)
Definition: properties.cpp:39
xml
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:107
count_properties
std::size_t count_properties(const propertiest &, property_statust)
Return the number of properties with given status.
Definition: properties.cpp:159
json
json_objectt json(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:127
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.
goto_program.h
Concrete Goto Program.
json_stream_objectt
Provides methods for streaming JSON objects.
Definition: json_stream.h:140
property_infot
Definition: properties.h:59
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:647
initialize_properties
propertiest initialize_properties(const abstract_goto_modelt &)
Returns the properties in the goto model.
Definition: properties.cpp:68
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:66
property_infot::property_infot
property_infot(goto_programt::const_targett pc, std::string description, property_statust status)
Definition: properties.cpp:60