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