Merge pull request #422 from ccadar/div-zero-test

Added test case exposing division by zero failure reported by @kren1 and made division total in STP to fix it.

2 files changed, 25 insertions, 0 deletions

diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp
index 5c49521e..f2500572 100644
--- a/lib/Solver/STPSolver.cpp
+++ b/lib/Solver/STPSolver.cpp
@@ -98,6 +98,8 @@ STPSolverImpl::STPSolverImpl(bool _useForkedSTP, bool _optimizeDivides)
   // we restore the old behaviour.
   vc_setInterfaceFlags(vc, EXPRDELETE, 0);
 
+  make_division_total(vc);
+
   vc_registerErrorHandler(::stp_error_handler);
 
   if (useForkedSTP) {
diff --git a/test/regression/2016-06-28-div-zero-bug.c b/test/regression/2016-06-28-div-zero-bug.c
new file mode 100644
index 00000000..11689aa0
--- /dev/null
+++ b/test/regression/2016-06-28-div-zero-bug.c
@@ -0,0 +1,23 @@
+// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --use-cex-cache=false %t.bc >%t1.log
+
+// This bug is triggered when using STP up to an including 2.1.0
+// See https://github.com/klee/klee/issues/308
+// and https://github.com/stp/stp/issues/206
+
+int b, a, g;
+
+int *c = &b, *d = &b, *f = &a;
+
+int safe_div(short p1, int p2) { 
+  return p2 == 0 ? p1 : p2; 
+}
+
+int main() {
+  klee_make_symbolic(&b, sizeof b);
+  if (safe_div(*c, 0))
+    *f = (int)&b % *c;
+
+  safe_div(a && g, *d);
+}