Merge pull request #6696 from tautschnig/feature/json-xml-property-info

Include source location in JSON/XML property output

Author: tautschnig

doc/assets/xml_spec.xsd

@@ -11,6 +11,7 @@
   <xs:complexType>
     <xs:attribute name="file" type="xs:string" use="optional"/>
     <xs:attribute name="line" type="xs:int" use="optional"/>
+    <xs:attribute name="column" type="xs:int" use="optional"/>
     <xs:attribute name="working-directory" type="xs:string"
                   use="optional"/>
     <xs:attribute name="function" type="xs:string" use="optional"/>
@@ -164,6 +165,7 @@
   <xs:element name="result">
     <xs:complexType>
       <xs:sequence>
+        <xs:element ref="location" minOccurs="0"/>
         <xs:element ref="goto_trace" minOccurs="0"/>
       </xs:sequence>
       <xs:attribute name="property" type="xs:string"/>

regression/cbmc/json-interface1/test.desc

@@ -5,8 +5,8 @@ activate-multi-line-match
 ^EXIT=10$
 ^SIGNAL=0$
 Not unwinding loop foo\.0 iteration 3 file main\.c line 5 function foo thread 0
-\{\n\s*"description": "assertion 0",\n\s*"property": "foo\.assertion\.(1|3)",\n\s*"status": "SUCCESS"\n\s*\}
-\{\n\s*"description": "assertion 0",\n\s*"property": "foo\.assertion\.(1|3)",\n\s*"status": "FAILURE",\n\s*"trace": \[
+\{\n\s*"description": "assertion 0",\n\s*"property": "foo\.assertion\.(1|3)",\n\s*"sourceLocation": \{\n\s*"file": "main.c",\n\s*"function": "foo",\n\s*"line": "(8|11)",\n\s*"workingDirectory": ".*json-interface1"\n\s*\},\n\s*"status": "SUCCESS"\n\s*\}
+\{\n\s*"description": "assertion 0",\n\s*"property": "foo\.assertion\.(1|3)",\n\s*"sourceLocation": \{\n\s*"file": "main.c",\n\s*"function": "foo",\n\s*"line": "(8|11)",\n\s*"workingDirectory": ".*json-interface1"\n\s*\},\n\s*"status": "FAILURE",\n\s*"trace": \[
 VERIFICATION FAILED
 --
 "property": "foo\.assertion\.2"

regression/cbmc/xml-interface1/test.desc

@@ -4,7 +4,7 @@ CORE
 ^EXIT=10$
 ^SIGNAL=0$
 Not unwinding loop foo\.0 iteration 3 file main\.c line 5 function foo thread 0
-<result property="foo\.assertion\.3" status="SUCCESS"/>
+<result property="foo\.assertion\.3" status="SUCCESS">
 <result property="foo\.assertion\.1" status="FAILURE">
 <goto_trace>
 VERIFICATION FAILED

src/goto-checker/properties.cpp

@@ -14,8 +14,10 @@ Author: Daniel Kroening, Peter Schrammel
 #include <util/exit_codes.h>
 #include <util/invariant.h>
 #include <util/json.h>
+#include <util/json_irep.h>
 #include <util/json_stream.h>
 #include <util/xml.h>
+#include <util/xml_irep.h>
 
 #include <goto-programs/abstract_goto_model.h>
 
@@ -110,6 +112,7 @@ xmlt xml(const irep_idt &property_id, const property_infot &property_info)
   xmlt xml_result("result");
   xml_result.set_attribute("property", id2string(property_id));
   xml_result.set_attribute("status", as_string(property_info.status));
+  xml_result.new_element(xml(property_info.pc->source_location()));
   return xml_result;
 }
 
@@ -122,6 +125,7 @@ static void json(
   result["property"] = json_stringt(property_id);
   result["description"] = json_stringt(property_info.description);
   result["status"] = json_stringt(as_string(property_info.status));
+  result["sourceLocation"] = json(property_info.pc->source_location());
 }
 
 json_objectt