CBMC
Loading...
Searching...
No Matches
properties.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Properties
4
5Author: 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 <map>
16
18
20class json_objectt;
22class xmlt;
23
26{
30 UNKNOWN,
34 PASS,
36 FAIL,
38 ERROR
39};
40
41std::string as_string(property_statust);
42
44enum class resultt
45{
47 UNKNOWN,
49 PASS,
51 FAIL,
53 ERROR
54};
55
56std::string as_string(resultt);
57
74
76typedef std::map<irep_idt, property_infot> propertiest;
77
80
83 propertiest &properties,
84 const abstract_goto_modelt &goto_model);
85
86std::string
87as_string(const irep_idt &property_id, const property_infot &property_info);
88
89xmlt xml(const irep_idt &property_id, const property_infot &property_info);
90
92json(const irep_idt &property_id, const property_infot &property_info);
93
95void json(json_stream_objectt &, const irep_idt &, const property_infot &);
96
98
100std::size_t count_properties(const propertiest &, property_statust);
101
104
106bool has_properties_to_check(const propertiest &properties);
107
110resultt determine_result(const propertiest &properties);
111
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...
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
instructionst::const_iterator const_targett
Provides methods for streaming JSON objects.
Definition xml.h:21
Concrete Goto Program.
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.
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
property_statust & operator&=(property_statust &, property_statust const &)
Update with the preference order.
resultt
The result of goto verifying.
Definition properties.h:45
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.
Definition properties.h:72
std::string description
A description (usually derived from the assertion's comment)
Definition properties.h:69
goto_programt::const_targett pc
A pointer to the corresponding goto instruction.
Definition properties.h:66