From b715ffa0c805f4d4813f0cda8b17eeb618e1ebf0 Mon Sep 17 00:00:00 2001 From: Timotej Kapus Date: Fri, 8 Nov 2019 12:25:59 +0000 Subject: [optimize-array] Fix hole index in buildMixedSelectExpr buildMixedSelectExpr was using the byte index for holes in the select condition instead of the word based one. This only occured if there was more than 1 hole. --- test/ArrayOpt/test_mixed_hole.c | 38 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) create mode 100644 test/ArrayOpt/test_mixed_hole.c (limited to 'test/ArrayOpt') 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 +#include + +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; +} -- cgit 1.4.1