about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2016-04-14 19:31:00 +0100
committerCristian Cadar <c.cadar@imperial.ac.uk>2016-04-14 19:31:00 +0100
commit7616398de27ac2aabfc707ba11fce33ef6032627 (patch)
tree4660f18088584e7bd61d5669e29c54fe27b26079
parentf9e074489f7542d29751f899c742803f186ca2cf (diff)
downloadklee-7616398de27ac2aabfc707ba11fce33ef6032627.tar.gz
Added test case with the examples from https://github.com/klee/klee/issues/334, which triggers a bug in solver-optimize-divides, and which is for now expected to fail.
-rw-r--r--test/regression/2016-04-14-sdiv-2.c25
1 files changed, 25 insertions, 0 deletions
diff --git a/test/regression/2016-04-14-sdiv-2.c b/test/regression/2016-04-14-sdiv-2.c
new file mode 100644
index 00000000..88a5fca3
--- /dev/null
+++ b/test/regression/2016-04-14-sdiv-2.c
@@ -0,0 +1,25 @@
+// XFAIL: *
+// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out -exit-on-error -solver-optimize-divides=true %t.bc >%t1.log
+// RUN: grep "m is 2" %t1.log
+
+#include <assert.h>
+
+int main(void)
+{
+  int n, m;
+  klee_make_symbolic(&n, sizeof n, "n");
+  klee_assume(n < -1);
+
+  if (n/2 > 0)
+    assert(0);
+
+  klee_make_symbolic(&m, sizeof m, "m");
+  klee_assume(m > 0);
+
+  if (m/2 == 2)
+    printf("m is 2\n");
+  
+  return 0;
+}