From f4dafa4acb5ad9ff02317f7df5bdae6974494fda Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Tue, 28 Jun 2016 19:14:37 +0100 Subject: Added test case exposing division by zero failure reported by @kren1, and recently fixed in STP. --- test/regression/2016-06-28-div-zero-bug.c | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 test/regression/2016-06-28-div-zero-bug.c 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); +} -- cgit 1.4.1 From 2cdbb892e93c3a6556fc4eb989ccd7cab8bfdb63 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Fri, 29 Jul 2016 18:49:26 +0100 Subject: Explicitely making division total in STP. --- lib/Solver/STPSolver.cpp | 2 ++ 1 file changed, 2 insertions(+) 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) { -- cgit 1.4.1