Add fault-localization regression tests

doc/assets/xml_spec.xsd

@@ -183,6 +183,27 @@
 
   <xs:element name="refinement-iteration" type="xs:integer"/>
 
+  <xs:element name="fault-localization">
+    <xs:complexType>
+      <xs:sequence>
+        <xs:element name="diagnosis">
+          <xs:complexType>
+            <xs:sequence>
+              <xs:element name="result">
+                <xs:complexType>
+                  <xs:sequence>
+                    <xs:element ref="location"/>
+                  </xs:sequence>
+                </xs:complexType>
+              </xs:element>
+            </xs:sequence>
+            <xs:attribute name="property" type="xs:string"/>
+          </xs:complexType>
+        </xs:element>
+      </xs:sequence>
+    </xs:complexType>
+  </xs:element>
+
   <xs:element name="program" type="xs:string"/>
   <xs:element name="cprover-status" type="xs:string"/>
   <xs:element name="cprover">
@@ -193,6 +214,7 @@
         <xs:element ref="message"/>
         <xs:element ref="result"/>
         <xs:element ref="refinement-iteration"/>
+        <xs:element ref="fault-localization"/>
        </xs:choice>
       <xs:element ref="cprover-status" minOccurs="0"/>
       </xs:sequence>

regression/cbmc/fault_localization-all_properties1/main.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+
+void main()
+{
+  int x, c;
+  if(c)
+    x = 0;
+  else
+    x++;
+  assert(x == 0);
+  assert(x != 0);
+}

regression/cbmc/fault_localization-all_properties1/test.desc

@@ -0,0 +1,12 @@
+KNOWNBUG
+main.c
+--localize-faults
+^EXIT=10$
+^SIGNAL=0$
+line 7 function main$
+line 9 function main$
+^VERIFICATION FAILED$
+--
+--
+With --localize-faults, CBMC only reports the first assertion as failing.
+Without --localize-faults, CBMC correctly reports both assertions as failing.

regression/cbmc/fault_localization-all_properties2/main.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+
+void main()
+{
+  int x, c;
+  if(c)
+    x = 0;
+  else
+    x++;
+  assert(x == 0);
+  assert(x == 0 || c == 0);
+}

regression/cbmc/fault_localization-all_properties2/test.desc

@@ -0,0 +1,11 @@
+KNOWNBUG
+main.c
+--localize-faults
+^EXIT=10$
+^SIGNAL=0$
+line 9 function main$
+^VERIFICATION FAILED$
+--
+--
+CBMC wrongly reports line 7 as the faulty statement when instead it should be
+line 9.

regression/cbmc/fault_localization-stop_on_fail1/main.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+
+void main()
+{
+  int x, c;
+  if(c)
+    x = 0;
+  else
+    x++;
+  assert(x == 0);
+  assert(x != 0);
+}

regression/fault-localization/stop_on_fail1/test.desc → regression/cbmc/fault_localization-stop_on_fail1/test.desc

@@ -1,9 +1,9 @@
-CORE
+CORE paths-lifo-expected-failure broken-smt-backend
 main.c
 --localize-faults --stop-on-fail
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.1\]:
+^\[main.assertion.[12]\]:
 line . function main$
 ^VERIFICATION FAILED$
 --

src/goto-checker/bmc_util.cpp

@@ -79,21 +79,22 @@ void output_error_trace(
 
   case ui_message_handlert::uit::XML_UI:
   {
-    xmlt xml;
-    convert(ns, goto_trace, xml);
-    msg.status() << xml;
+    const goto_trace_stept &last_step = goto_trace.get_last_step();
+    property_infot info{
+      last_step.pc, last_step.comment, property_statust::FAIL};
+    xmlt xml_result = xml(last_step.property_id, info);
+    convert(ns, goto_trace, xml_result.new_element());
+    msg.result() << xml_result;
   }
   break;
 
   case ui_message_handlert::uit::JSON_UI:
   {
     json_stream_objectt &json_result =
       ui_message_handler.get_json_stream().push_back_stream_object();
-    const goto_trace_stept &step = goto_trace.steps.back();
-    json_result["property"] =
-      json_stringt(step.pc->source_location.get_property_id());
-    json_result["description"] =
-      json_stringt(step.pc->source_location.get_comment());
+    const goto_trace_stept &step = goto_trace.get_last_step();
+    json_result["property"] = json_stringt(step.property_id);
+    json_result["description"] = json_stringt(step.comment);
     json_result["status"] = json_stringt("failed");
     json_stream_arrayt &json_trace =
       json_result.push_back_stream_array("trace");