Merge pull request #5934 from tautschnig/fault-localization-tests

Add fault-localization regression tests

Author: tautschnig

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 renamed to 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$
 --