diff options
| -rw-r--r-- | lib/Expr/ArrayExprOptimizer.cpp | 3 | ||||
| -rw-r--r-- | test/ArrayOpt/test_mixed_hole.c | 38 |
2 files changed, 39 insertions, 2 deletions
diff --git a/lib/Expr/ArrayExprOptimizer.cpp b/lib/Expr/ArrayExprOptimizer.cpp index 8ba0b40d..b55974d0 100644 --- a/lib/Expr/ArrayExprOptimizer.cpp +++ b/lib/Expr/ArrayExprOptimizer.cpp @@ -643,8 +643,7 @@ ref<Expr> ExprOptimizer::buildMixedSelectExpr( ref<Expr> temp_idx = MulExpr::create( ConstantExpr::create(holes[i], re->index->getWidth()), ConstantExpr::create(width / 8, re->index->getWidth())); - ref<Expr> cond = EqExpr::create( - re->index, ConstantExpr::create(holes[i], re->index->getWidth())); + ref<Expr> cond = EqExpr::create(re->index, temp_idx); ref<Expr> temp = SelectExpr::create( cond, extendRead(re->updates, temp_idx, width), result); result = temp; diff --git a/test/ArrayOpt/test_mixed_hole.c b/test/ArrayOpt/test_mixed_hole.c new file mode 100644 index 00000000..1a95a5ef --- /dev/null +++ b/test/ArrayOpt/test_mixed_hole.c @@ -0,0 +1,38 @@ +// RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --optimize-array=value --use-query-log=all:kquery --write-kqueries --output-dir=%t.klee-out %t.bc > %t.log 2>&1 +// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V +// RUN: FileCheck %s -input-file=%t.log + +// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful +// CHECK-CONST_ARR: const_arr + +#include "klee/klee.h" +#include <assert.h> +#include <stdio.h> + +short array[6] = {1, 2, 3, 4, 5, 0}; + +int main() { + char idx; + short symHole, symHole2; + klee_make_symbolic(&symHole, sizeof(symHole), "hole"); + klee_make_symbolic(&symHole2, sizeof(symHole2), "hole2"); + klee_make_symbolic(&idx, sizeof(idx), "idx"); + klee_assume(idx < 5); + klee_assume(idx > 0); + klee_assume((symHole < 401) & (symHole > 399)); + klee_assume(symHole2 != 400); + array[2] = symHole; + array[0] = symHole2; + + // CHECK: KLEE: done: completed paths = 2 + // CHECK: Yes + // CHECK-NEXT: No + if (array[idx + 1] == 400) + printf("Yes\n"); + else + printf("No\n"); + + return 0; +} |