From cc267845c8a4f954cdf9402ade03196be16148ea Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Thu, 14 Apr 2016 22:39:47 +0100 Subject: This test passes under 2.9, so it cannot be used as an XFAIL. We can enable it after the division bug is fixed. --- test/regression/2016-04-14-sdiv-2.c | 25 ------------------------- test/regression/2016-04-14-sdiv-2.c_ | 25 +++++++++++++++++++++++++ 2 files changed, 25 insertions(+), 25 deletions(-) delete mode 100644 test/regression/2016-04-14-sdiv-2.c create mode 100644 test/regression/2016-04-14-sdiv-2.c_ (limited to 'test') diff --git a/test/regression/2016-04-14-sdiv-2.c b/test/regression/2016-04-14-sdiv-2.c deleted file mode 100644 index 88a5fca3..00000000 --- a/test/regression/2016-04-14-sdiv-2.c +++ /dev/null @@ -1,25 +0,0 @@ -// 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; -} 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