basic tests for fault localization

Author: Peter Schrammel

regression/fault-localization/Makefile

@@ -0,0 +1,20 @@
+default: tests.log
+
+test:
+	@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
+
+tests.log: ../test.pl
+	@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;

regression/fault-localization/all_properties1/main.c

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

regression/fault-localization/all_properties1/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--localize-faults
+^EXIT=10$
+^SIGNAL=0$
+line 7 function main$
+line 6 function main$
+^VERIFICATION FAILED$
+--

regression/fault-localization/all_properties2/main.c

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

regression/fault-localization/all_properties2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--localize-faults
+^EXIT=10$
+^SIGNAL=0$
+line 7 function main$
+^VERIFICATION FAILED$
+--

regression/fault-localization/stop_on_fail1/main.c

@@ -0,0 +1,10 @@
+#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

@@ -0,0 +1,9 @@
+CORE
+main.c
+--localize-faults --stop-on-fail
+^EXIT=10$
+^SIGNAL=0$
+^\[main.assertion.1\]:
+line . function main$
+^VERIFICATION FAILED$
+--