Merge pull request #26 from delcypher/fix_divide_by_zero

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

2 files changed, 56 insertions, 0 deletions

diff --git a/test/Feature/OvershiftCheck.c b/test/Feature/OvershiftCheck.c
new file mode 100644
index 00000000..bb967166
--- /dev/null
+++ b/test/Feature/OvershiftCheck.c
@@ -0,0 +1,26 @@
+// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
+// RUN: %klee -check-overshift %t.bc 2> %t.log
+// RUN: grep -c "overshift error" %t.log
+// RUN: grep -c "OvershiftCheck.c:19: overshift error" %t.log
+// RUN: grep -c "OvershiftCheck.c:23: overshift error" %t.log
+
+/* This test checks that two consecutive potential overshifts
+ * are reported as errors.
+ */
+int main()
+{
+  unsigned int x=15;
+  unsigned int y;
+  unsigned int z;
+  volatile unsigned int result;
+
+  /* Overshift if y>= sizeof(x) */
+  klee_make_symbolic(&y,sizeof(y),"shift_amount1");
+  result = x << y;
+
+  /* Overshift is z>= sizeof(x) */
+  klee_make_symbolic(&z,sizeof(z),"shift_amount2");
+  result = x >> z;
+
+  return 0;
+}
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;
+}