diff options
| -rw-r--r-- | lib/Solver/STPSolver.cpp | 2 | ||||
| -rw-r--r-- | test/regression/2016-06-28-div-zero-bug.c | 23 |
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); +} |