Add fault-localization regression tests

Moving the (three) tests from a dedicated folder to cbmc to run them,
also making use of all three configurations that the cbmc folder is
being tested with.

Author: tautschnig

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);
+}

…ult-localization/stop_on_fail1/test.desc …ult_localization-stop_on_fail1/test.descregression/fault-localization/stop_on_fail1/test.desc renamed to regression/cbmc/fault_localization-stop_on_fail1/test.desc 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$
 --