diff options
| -rw-r--r-- | lib/Solver/STPBuilder.cpp | 2 | ||||
| -rw-r--r-- | test/Feature/srem.c | 33 |
2 files changed, 34 insertions, 1 deletions
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index c2f23c0a..ddeb3c37 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -751,7 +751,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) { #endif // XXX implement my fast path and test for proper handling of sign - return vc_sbvModExpr(vc, *width_out, left, right); + return vc_sbvRemExpr(vc, *width_out, left, right); } // Bitwise diff --git a/test/Feature/srem.c b/test/Feature/srem.c new file mode 100644 index 00000000..f4fa8aa5 --- /dev/null +++ b/test/Feature/srem.c @@ -0,0 +1,33 @@ +// 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=1 %t.bc +// RUN: grep "KLEE: done: explored paths = 5" %t.klee-out/info +// RUN: grep "KLEE: done: generated tests = 4" %t.klee-out/info +#include <stdio.h> +#include <assert.h> + +int main(int argc, char** argv) +{ + int y; + + klee_make_symbolic(&y, sizeof(y), "y"); + + // Test cases divisor is positive or negative + if (y >= 0) { + if (y < 2) { + // Two test cases generated taking this path, one for y == 0 and y ==1 + assert(1 % y == 0); + } else { + assert(1 % y == 1); + } + } else { + if (y > -2) { + assert(1 % y == 0); + } else { + assert(1 % y == 1); + } + } + + assert(0 % y == 0); + assert(-1 % y == -1); +} |