Fixed bug where divide by zero bugs would only be detected once in a program

even if there were many divide by zero bugs.

The fix basically inlines all function calls to klee_div_zero_check()
so that each call to klee_report_error() is a unique instruction
for each instrumentation of a divide operation.

It also seems that inlining the call "magically" fixed the debug information
(file and line number) of the instruction so that the debug information on the
inlined instructions matches that of the instrumented division instruction.

Note that the command line option -emit-all-errors could be used to
workaround the bug fixed in this commit.

1 files changed, 30 insertions, 0 deletions

diff --git a/test/Feature/consecutive_divide_by_zero.c b/test/Feature/consecutive_divide_by_zero.c
new file mode 100644
index 00000000..c1185870
--- /dev/null
+++ b/test/Feature/consecutive_divide_by_zero.c
@@ -0,0 +1,30 @@
+// RUN: %llvmgcc -emit-llvm -c -g -O0 %s -o %t.bc
+// RUN: %klee -check-div-zero -emit-all-errors=0 %t.bc 2> %t.log
+// RUN: grep "completed paths = 3" %t.log
+// RUN: grep "generated tests = 3" %t.log
+// RUN: grep "consecutive_divide_by_zero.c:24: divide by zero" %t.log
+// RUN: grep "consecutive_divide_by_zero.c:27: divide by zero" %t.log
+
+/* This test case captures a bug where two distinct division
+*  by zero errors are treated as the same error and so
+*  only one test case is generated EVEN IF THERE ARE MULTIPLE 
+*  DISTINCT ERRORS!
+*/
+int main()
+{
+  unsigned int a=15;
+  unsigned int b=15;
+  volatile unsigned int d1;
+  volatile unsigned int d2;
+
+  klee_make_symbolic(&d1, sizeof(d1),"divisor1");
+  klee_make_symbolic(&d2, sizeof(d2),"divisor2");
+
+  // deliberate division by zero possible
+  unsigned int result1 = a / d1;
+
+  // another deliberate division by zero possible
+  unsigned int result2 = b / d2;
+
+  return 0;
+}