Skip to content

Commit b10cd3d

Browse files
committed
Include source location in JSON/XML property output
Unlike the plain-text variant, neither JSON nor XML included source locations for each of the properties being reported upon by a goto-checker. Fixes: #6651
1 parent 7157df5 commit b10cd3d

File tree

1 file changed

+4
-0
lines changed

1 file changed

+4
-0
lines changed

src/goto-checker/properties.cpp

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,8 +14,10 @@ Author: Daniel Kroening, Peter Schrammel
1414
#include <util/exit_codes.h>
1515
#include <util/invariant.h>
1616
#include <util/json.h>
17+
#include <util/json_irep.h>
1718
#include <util/json_stream.h>
1819
#include <util/xml.h>
20+
#include <util/xml_irep.h>
1921

2022
#include <goto-programs/abstract_goto_model.h>
2123

@@ -110,6 +112,7 @@ xmlt xml(const irep_idt &property_id, const property_infot &property_info)
110112
xmlt xml_result("result");
111113
xml_result.set_attribute("property", id2string(property_id));
112114
xml_result.set_attribute("status", as_string(property_info.status));
115+
xml_result.new_element(xml(property_info.pc->source_location()));
113116
return xml_result;
114117
}
115118

@@ -122,6 +125,7 @@ static void json(
122125
result["property"] = json_stringt(property_id);
123126
result["description"] = json_stringt(property_info.description);
124127
result["status"] = json_stringt(as_string(property_info.status));
128+
result["sourceLocation"] = json(property_info.pc->source_location());
125129
}
126130

127131
json_objectt

0 commit comments

Comments
 (0)