From 7616398de27ac2aabfc707ba11fce33ef6032627 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Thu, 14 Apr 2016 19:31:00 +0100 Subject: 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. --- test/regression/2016-04-14-sdiv-2.c | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) create mode 100644 test/regression/2016-04-14-sdiv-2.c (limited to 'test/regression') 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 + +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; +} -- cgit 1.4.1