Skip to content

Commit c00fd37

Browse files
Add property output functions
Plain text, XML and JSON output for property results.
1 parent d7a8156 commit c00fd37

File tree

2 files changed

+38
-0
lines changed

2 files changed

+38
-0
lines changed

src/goto-checker/properties.cpp

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,8 @@ Author: Daniel Kroening, Peter Schrammel
1212
#include "properties.h"
1313

1414
#include <util/invariant.h>
15+
#include <util/json.h>
16+
#include <util/xml.h>
1517

1618
std::string as_string(resultt result)
1719
{
@@ -79,6 +81,31 @@ propertiest initialize_properties(const abstract_goto_modelt &goto_model)
7981
return properties;
8082
}
8183

84+
std::string
85+
as_string(const irep_idt &property_id, const property_infot &property_info)
86+
{
87+
return "[" + id2string(property_id) + "] " + property_info.description +
88+
": " + as_string(property_info.result);
89+
}
90+
91+
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
92+
{
93+
xmlt xml_result("result");
94+
xml_result.set_attribute("property", id2string(property_id));
95+
xml_result.set_attribute("status", as_string(property_info.result));
96+
return xml_result;
97+
}
98+
99+
json_objectt
100+
json(const irep_idt &property_id, const property_infot &property_info)
101+
{
102+
json_objectt result;
103+
result["property"] = json_stringt(property_id);
104+
result["description"] = json_stringt(property_info.description);
105+
result["status"] = json_stringt(as_string(property_info.result));
106+
return result;
107+
}
108+
82109
/// Returns the number of properties with given \p result
83110
std::size_t
84111
count_properties(const propertiest &properties, property_resultt result)

src/goto-checker/properties.h

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,9 @@ Author: Daniel Kroening, Peter Schrammel
1616

1717
#include <goto-programs/goto_model.h>
1818

19+
class json_objectt;
20+
class xmlt;
21+
1922
/// The result status of a property
2023
enum class property_resultt
2124
{
@@ -68,6 +71,14 @@ typedef std::unordered_map<irep_idt, property_infot> propertiest;
6871
/// Returns the properties in the goto model
6972
propertiest initialize_properties(const abstract_goto_modelt &);
7073

74+
std::string
75+
as_string(const irep_idt &property_id, const property_infot &property_info);
76+
77+
xmlt xml(const irep_idt &property_id, const property_infot &property_info);
78+
79+
json_objectt
80+
json(const irep_idt &property_id, const property_infot &property_info);
81+
7182
std::size_t
7283
count_properties(const propertiest &properties, property_resultt result);
7384

0 commit comments

Comments
 (0)