From f4dafa4acb5ad9ff02317f7df5bdae6974494fda Mon Sep 17 00:00:00 2001
From: Cristian Cadar <c.cadar@imperial.ac.uk>
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

(limited to 'test')

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