cprover
|
Properties. More...
Go to the source code of this file.
Classes | |
struct | property_infot |
Typedefs | |
typedef std::unordered_map< irep_idt, property_infot > | propertiest |
A map of property IDs to property infos. More... | |
Enumerations | |
enum | property_statust { property_statust::NOT_CHECKED, property_statust::UNKNOWN, property_statust::NOT_REACHABLE, property_statust::PASS, property_statust::FAIL, property_statust::ERROR } |
The status of a property. More... | |
enum | resultt { resultt::UNKNOWN, resultt::PASS, resultt::FAIL, resultt::ERROR } |
The result of goto verifying. More... | |
Functions | |
std::string | as_string (property_statust) |
std::string | as_string (resultt) |
propertiest | initialize_properties (const abstract_goto_modelt &) |
Returns the properties in the goto model. More... | |
void | update_properties_from_goto_model (propertiest &properties, const abstract_goto_modelt &goto_model) |
Updates properties with the assertions in goto_model . More... | |
std::string | as_string (const irep_idt &property_id, const property_infot &property_info) |
xmlt | xml (const irep_idt &property_id, const property_infot &property_info) |
json_objectt | json (const irep_idt &property_id, const property_infot &property_info) |
void | json (json_stream_objectt &, const irep_idt &, const property_infot &) |
Write the property info into the given JSON stream object. More... | |
int | result_to_exit_code (resultt result) |
std::size_t | count_properties (const propertiest &, property_statust) |
Return the number of properties with given status . More... | |
bool | is_property_to_check (property_statust) |
Return true if the status is NOT_CHECKED or UNKNOWN. More... | |
bool | has_properties_to_check (const propertiest &properties) |
Return true if there as a property with NOT_CHECKED or UNKNOWN status. More... | |
property_statust & | operator|= (property_statust &, property_statust const &) |
Update with the preference order. More... | |
property_statust & | operator&= (property_statust &, property_statust const &) |
Update with the preference order. More... | |
resultt | determine_result (const propertiest &properties) |
Determines the overall result corresponding from the given properties That is PASS if all properties are PASS or NOT_CHECKED, FAIL if at least one property is FAIL and no property is ERROR, UNKNOWN if no property is FAIL or ERROR and at least one property is UNKNOWN, ERROR if at least one property is error. More... | |
Properties.
Definition in file properties.h.
typedef std::unordered_map<irep_idt, property_infot> propertiest |
A map of property IDs to property infos.
Definition at line 75 of file properties.h.
|
strong |
The status of a property.
Definition at line 24 of file properties.h.
|
strong |
The result of goto verifying.
Enumerator | |
---|---|
UNKNOWN | No property was violated, neither was there an error. |
PASS | No properties were violated. |
FAIL | Some properties were violated. |
ERROR | An error occurred during goto checking. |
Definition at line 43 of file properties.h.
std::string as_string | ( | const irep_idt & | property_id, |
const property_infot & | property_info | ||
) |
Definition at line 99 of file properties.cpp.
std::string as_string | ( | property_statust | ) |
Definition at line 37 of file properties.cpp.
std::string as_string | ( | resultt | ) |
Definition at line 20 of file properties.cpp.
std::size_t count_properties | ( | const propertiest & | , |
property_statust | |||
) |
Return the number of properties with given status
.
Definition at line 157 of file properties.cpp.
resultt determine_result | ( | const propertiest & | properties | ) |
Determines the overall result corresponding from the given properties That is PASS if all properties are PASS or NOT_CHECKED, FAIL if at least one property is FAIL and no property is ERROR, UNKNOWN if no property is FAIL or ERROR and at least one property is UNKNOWN, ERROR if at least one property is error.
Definition at line 258 of file properties.cpp.
bool has_properties_to_check | ( | const propertiest & | properties | ) |
Return true if there as a property with NOT_CHECKED or UNKNOWN status.
Definition at line 174 of file properties.cpp.
propertiest initialize_properties | ( | const abstract_goto_modelt & | ) |
Returns the properties in the goto model.
Definition at line 66 of file properties.cpp.
bool is_property_to_check | ( | property_statust | ) |
Return true if the status is NOT_CHECKED or UNKNOWN.
Definition at line 168 of file properties.cpp.
json_objectt json | ( | const irep_idt & | property_id, |
const property_infot & | property_info | ||
) |
Definition at line 125 of file properties.cpp.
void json | ( | json_stream_objectt & | , |
const irep_idt & | , | ||
const property_infot & | |||
) |
Write the property info into the given JSON stream object.
Definition at line 132 of file properties.cpp.
property_statust& operator&= | ( | property_statust & | a, |
property_statust const & | b | ||
) |
Update with the preference order.
Definition at line 224 of file properties.cpp.
property_statust& operator|= | ( | property_statust & | a, |
property_statust const & | b | ||
) |
Update with the preference order.
Definition at line 190 of file properties.cpp.
int result_to_exit_code | ( | resultt | result | ) |
Definition at line 140 of file properties.cpp.
void update_properties_from_goto_model | ( | propertiest & | properties, |
const abstract_goto_modelt & | goto_model | ||
) |
Updates properties
with the assertions in goto_model
.
Definition at line 73 of file properties.cpp.
xmlt xml | ( | const irep_idt & | property_id, |
const property_infot & | property_info | ||
) |
Definition at line 105 of file properties.cpp.