about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2016-06-28 19:14:37 +0100
committerCristian Cadar <c.cadar@imperial.ac.uk>2016-06-28 19:14:37 +0100
commitf4dafa4acb5ad9ff02317f7df5bdae6974494fda (patch)
treecaf5a9e612f11100ac6524dfba23712bdad0e6fc
parente5a958a8e10fa2f52e071dffc6c77dcc6356f074 (diff)
downloadklee-f4dafa4acb5ad9ff02317f7df5bdae6974494fda.tar.gz
Added test case exposing division by zero failure reported by @kren1, and recently fixed in STP.
-rw-r--r--test/regression/2016-06-28-div-zero-bug.c23
1 files changed, 23 insertions, 0 deletions
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);
+}