|
CBMC
|
#include <properties.h>
Collaboration diagram for property_infot:Public Member Functions | |
| property_infot (goto_programt::const_targett pc, std::string description, property_statust status) | |
Public Attributes | |
| goto_programt::const_targett | pc |
| A pointer to the corresponding goto instruction. More... | |
| std::string | description |
| A description (usually derived from the assertion's comment) More... | |
| property_statust | status |
| The status of the property. More... | |
Definition at line 58 of file properties.h.
| property_infot::property_infot | ( | goto_programt::const_targett | pc, |
| std::string | description, | ||
| property_statust | status | ||
| ) |
Definition at line 62 of file properties.cpp.
| std::string property_infot::description |
A description (usually derived from the assertion's comment)
Definition at line 69 of file properties.h.
| goto_programt::const_targett property_infot::pc |
A pointer to the corresponding goto instruction.
Definition at line 66 of file properties.h.
| property_statust property_infot::status |
The status of the property.
Definition at line 72 of file properties.h.