From 61bb349e953d76bf3fd96a6f853f273f81ed13ff Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Fri, 15 Apr 2016 08:54:56 +0000 Subject: Fix variable shifting behavior with different sizes Generated STP equality expressions have to be the same type. If a shift with different types as operands was used, therefore equality expressions of different width were generated. Beside avoiding the different sizes, this patch restores the original behavior to extract just the part involved in shifting and therefore should generate smaller expressions. Enable sdiv test case --- test/regression/2016-04-14-sdiv-2.c | 26 ++++++++++++++++++++++++++ test/regression/2016-04-14-sdiv-2.c_ | 25 ------------------------- 2 files changed, 26 insertions(+), 25 deletions(-) create mode 100644 test/regression/2016-04-14-sdiv-2.c delete 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 new file mode 100644 index 00000000..974036ee --- /dev/null +++ b/test/regression/2016-04-14-sdiv-2.c @@ -0,0 +1,26 @@ +// 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 +#include + +#include "klee/klee.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; +} 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; -} -- cgit 1.4.1