1/*******************************************************************\
5Author: Daniel Kroening, Peter Schrammel
7\*******************************************************************/
12#ifndef CPROVER_GOTO_CHECKER_PROPERTIES_H
13#define CPROVER_GOTO_CHECKER_PROPERTIES_H
112#endif // CPROVER_GOTO_CHECKER_PROPERTIES_H
Abstract interface to eager or lazy GOTO models.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
instructionst::const_iterator const_targett
Provides methods for streaming JSON objects.
bool is_property_to_check(property_statust)
Return true if the status is NOT_CHECKED or UNKNOWN.
property_statust & operator|=(property_statust &, property_statust const &)
Update with the preference order.
propertiest initialize_properties(const abstract_goto_modelt &)
Returns the properties in the goto model.
bool has_properties_to_check(const propertiest &properties)
Return true if there as a property with NOT_CHECKED or UNKNOWN status.
property_statust
The status of a property.
@ 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.
property_statust & operator&=(property_statust &, property_statust const &)
Update with the preference order.
resultt
The result of goto verifying.
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 &, property_statust)
Return the number of properties with given status.
json_objectt json(const irep_idt &property_id, const property_infot &property_info)
int result_to_exit_code(resultt result)
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
std::string as_string(property_statust)
property_statust status
The status of the property.
std::string description
A description (usually derived from the assertion's comment)
goto_programt::const_targett pc
A pointer to the corresponding goto instruction.