diff options
author | Andrea Mattavelli <andreamattavelli@gmail.com> | 2017-11-22 17:18:07 +0000 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2018-10-23 18:53:46 +0300 |
commit | a53fade6e85394ef95dfaaa1c264149e85ea5451 (patch) | |
tree | e8d10b1cd288c0b013b5dc8039bdb3b8dbf42d8d /test/ArrayOpt/test_const_arr-idx.c | |
parent | 916b72a7955cbb06d1a10640f8c6daea14da523e (diff) | |
download | klee-a53fade6e85394ef95dfaaa1c264149e85ea5451.tar.gz |
Added support for KLEE index-based array optimization
Diffstat (limited to 'test/ArrayOpt/test_const_arr-idx.c')
-rw-r--r-- | test/ArrayOpt/test_const_arr-idx.c | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/test/ArrayOpt/test_const_arr-idx.c b/test/ArrayOpt/test_const_arr-idx.c new file mode 100644 index 00000000..25f959a3 --- /dev/null +++ b/test/ArrayOpt/test_const_arr-idx.c @@ -0,0 +1,26 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=index %t.bc > %t.log 2>&1 +// RUN: not FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I + +// CHECK-OPT_I: KLEE: WARNING: OPT_I: successful +// CHECK-CONST_ARR: const_arr + +#include <stdio.h> +#include "klee/klee.h" + +unsigned array[5] = {1,2,3,4,5}; +int arr[3] = {0,1,2}; + +int main() { + int x = 2; + unsigned k = arr[x]; + + // CHECK: Yes + if (array[k] == 3) + printf("Yes\n"); + + // CHECK: KLEE: done: completed paths = 1 + + return 0; +} |