diff options
| author | Martin Nowack <martin.nowack@gmail.com> | 2016-04-15 08:54:56 +0000 |
|---|---|---|
| committer | Martin Nowack <martin@se.inf.tu-dresden.de> | 2016-07-09 00:38:14 +0200 |
| commit | 61bb349e953d76bf3fd96a6f853f273f81ed13ff (patch) | |
| tree | de7ce7fcce647ec650630a071b5d570d54a1cedf /test/regression | |
| parent | e87e5bd478d8dad5a7c164197b9e39da3873442d (diff) | |
| download | klee-61bb349e953d76bf3fd96a6f853f273f81ed13ff.tar.gz | |
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
Diffstat (limited to 'test/regression')
| -rw-r--r-- | test/regression/2016-04-14-sdiv-2.c (renamed from test/regression/2016-04-14-sdiv-2.c_) | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/test/regression/2016-04-14-sdiv-2.c_ b/test/regression/2016-04-14-sdiv-2.c index 88a5fca3..974036ee 100644 --- a/test/regression/2016-04-14-sdiv-2.c_ +++ b/test/regression/2016-04-14-sdiv-2.c @@ -1,10 +1,11 @@ -// 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> +#include <stdio.h> + +#include "klee/klee.h" int main(void) { |