about summary refs log tree commit diff homepage
path: root/test/ArrayOpt
diff options
context:
space:
mode:
authorAndrea Mattavelli <andreamattavelli@gmail.com>2017-11-22 18:01:29 +0000
committerCristian Cadar <c.cadar@imperial.ac.uk>2018-10-23 18:53:46 +0300
commit1a9662670ebdef07269e1abfc3f0315bdb33277c (patch)
treeb9cb5938af34aefc6b960d0f666b82a1b29ffde1 /test/ArrayOpt
parenta53fade6e85394ef95dfaaa1c264149e85ea5451 (diff)
downloadklee-1a9662670ebdef07269e1abfc3f0315bdb33277c.tar.gz
Added support for KLEE value-based array optimization
Diffstat (limited to 'test/ArrayOpt')
-rw-r--r--test/ArrayOpt/test-mix.c56


-rw-r--r--test/ArrayOpt/test_array_index_array.c15


-rw-r--r--test/ArrayOpt/test_array_index_array_diffsize.c15


-rw-r--r--test/ArrayOpt/test_cache.c31


-rw-r--r--test/ArrayOpt/test_const_arr-idx.c7


-rw-r--r--test/ArrayOpt/test_expr_complex.c15


-rw-r--r--test/ArrayOpt/test_expr_simple.c15


-rw-r--r--test/ArrayOpt/test_feasible.c15


-rw-r--r--test/ArrayOpt/test_multindex.c15


-rw-r--r--test/ArrayOpt/test_new.c15


-rw-r--r--test/ArrayOpt/test_nier.c15


-rw-r--r--test/ArrayOpt/test_noncontiguous_idx.c16


-rw-r--r--test/ArrayOpt/test_position.c15


-rw-r--r--test/ArrayOpt/test_sub_idx.c15


-rw-r--r--test/ArrayOpt/test_var_idx.c15


15 files changed, 275 insertions, 0 deletions
diff --git a/test/ArrayOpt/test-mix.c b/test/ArrayOpt/test-mix.c
index 88cb595c..3b3d7a0f 100644
--- a/test/ArrayOpt/test-mix.c
+++ b/test/ArrayOpt/test-mix.c
@@ -26,8 +26,64 @@
 // RUN: not FileCheck %s -input-file=%t.klee-out/test000010.kquery -check-prefix=CHECK-CONST_ARR
 // RUN: not FileCheck %s -input-file=%t.klee-out/test000011.kquery -check-prefix=CHECK-CONST_ARR
 // RUN: not FileCheck %s -input-file=%t.klee-out/test000012.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=value %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V
+// RUN: test -f %t.klee-out/test000001.kquery
+// RUN: test -f %t.klee-out/test000002.kquery
+// RUN: test -f %t.klee-out/test000003.kquery
+// RUN: test -f %t.klee-out/test000004.kquery
+// RUN: test -f %t.klee-out/test000005.kquery
+// RUN: test -f %t.klee-out/test000006.kquery
+// RUN: test -f %t.klee-out/test000007.kquery
+// RUN: test -f %t.klee-out/test000008.kquery
+// RUN: test -f %t.klee-out/test000009.kquery
+// RUN: test -f %t.klee-out/test000010.kquery
+// RUN: test -f %t.klee-out/test000011.kquery
+// RUN: test -f %t.klee-out/test000012.kquery
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000003.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000004.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000005.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000006.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000007.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000008.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000009.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000010.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000011.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000012.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=all %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V
+// RUN: test -f %t.klee-out/test000001.kquery
+// RUN: test -f %t.klee-out/test000002.kquery
+// RUN: test -f %t.klee-out/test000003.kquery
+// RUN: test -f %t.klee-out/test000004.kquery
+// RUN: test -f %t.klee-out/test000005.kquery
+// RUN: test -f %t.klee-out/test000006.kquery
+// RUN: test -f %t.klee-out/test000007.kquery
+// RUN: test -f %t.klee-out/test000008.kquery
+// RUN: test -f %t.klee-out/test000009.kquery
+// RUN: test -f %t.klee-out/test000010.kquery
+// RUN: test -f %t.klee-out/test000011.kquery
+// RUN: test -f %t.klee-out/test000012.kquery
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000003.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000004.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000005.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000006.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000007.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000008.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000009.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000010.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000011.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000012.kquery -check-prefix=CHECK-CONST_ARR
 
 // CHECK-OPT_I: KLEE: WARNING: OPT_I: successful
+// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful
 // CHECK-CONST_ARR: const_arr
 
 #include <stdio.h>
diff --git a/test/ArrayOpt/test_array_index_array.c b/test/ArrayOpt/test_array_index_array.c
index 7d5198e1..cf852494 100644
--- a/test/ArrayOpt/test_array_index_array.c
+++ b/test/ArrayOpt/test_array_index_array.c
@@ -6,8 +6,23 @@
 // RUN: test -f %t.klee-out/test000002.kquery
 // RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
 // RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=value %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V
+// RUN: test -f %t.klee-out/test000001.kquery
+// RUN: test -f %t.klee-out/test000002.kquery
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=all %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V
+// RUN: test -f %t.klee-out/test000001.kquery
+// RUN: test -f %t.klee-out/test000002.kquery
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
 
 // CHECK-OPT_I: KLEE: WARNING: OPT_I: successful
+// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful
 // CHECK-CONST_ARR: const_arr
 
 #include <stdio.h>
diff --git a/test/ArrayOpt/test_array_index_array_diffsize.c b/test/ArrayOpt/test_array_index_array_diffsize.c
index e331f909..76ac08b2 100644
--- a/test/ArrayOpt/test_array_index_array_diffsize.c
+++ b/test/ArrayOpt/test_array_index_array_diffsize.c
@@ -6,8 +6,23 @@
 // RUN: test -f %t.klee-out/test000002.kquery
 // RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
 // RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=value %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V
+// RUN: test -f %t.klee-out/test000001.kquery
+// RUN: test -f %t.klee-out/test000002.kquery
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=all %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V
+// RUN: test -f %t.klee-out/test000001.kquery
+// RUN: test -f %t.klee-out/test000002.kquery
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
 
 // CHECK-OPT_I: KLEE: WARNING: OPT_I: successful
+// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful
 // CHECK-CONST_ARR: const_arr
 
 #include <stdio.h>
diff --git a/test/ArrayOpt/test_cache.c b/test/ArrayOpt/test_cache.c
index a2fe10da..2bc64fa4 100644
--- a/test/ArrayOpt/test_cache.c
+++ b/test/ArrayOpt/test_cache.c
@@ -14,8 +14,39 @@
 // RUN: not FileCheck %s -input-file=%t.klee-out/test000004.kquery -check-prefix=CHECK-CONST_ARR
 // RUN: not FileCheck %s -input-file=%t.klee-out/test000005.kquery -check-prefix=CHECK-CONST_ARR
 // RUN: not FileCheck %s -input-file=%t.klee-out/test000006.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=value %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V
+// RUN: test -f %t.klee-out/test000001.kquery
+// RUN: test -f %t.klee-out/test000002.kquery
+// RUN: test -f %t.klee-out/test000003.kquery
+// RUN: test -f %t.klee-out/test000004.kquery
+// RUN: test -f %t.klee-out/test000005.kquery
+// RUN: test -f %t.klee-out/test000006.kquery
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000003.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000004.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000005.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000006.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=all %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I
+// RUN: test -f %t.klee-out/test000001.kquery
+// RUN: test -f %t.klee-out/test000002.kquery
+// RUN: test -f %t.klee-out/test000003.kquery
+// RUN: test -f %t.klee-out/test000004.kquery
+// RUN: test -f %t.klee-out/test000005.kquery
+// RUN: test -f %t.klee-out/test000006.kquery
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000003.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000004.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000005.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000006.kquery -check-prefix=CHECK-CONST_ARR
 
 // CHECK-OPT_I: KLEE: WARNING: OPT_I: successful
+// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful
 // CHECK-CONST_ARR: const_arr
 
 #include <stdio.h>
diff --git a/test/ArrayOpt/test_const_arr-idx.c b/test/ArrayOpt/test_const_arr-idx.c
index 25f959a3..9b8a7272 100644
--- a/test/ArrayOpt/test_const_arr-idx.c
+++ b/test/ArrayOpt/test_const_arr-idx.c
@@ -2,8 +2,15 @@
 // 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
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=value %t.bc > %t.log 2>&1
+// RUN: not FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=all %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-OPT_V: KLEE: WARNING: OPT_V: successful
 // CHECK-CONST_ARR: const_arr
 
 #include <stdio.h>
diff --git a/test/ArrayOpt/test_expr_complex.c b/test/ArrayOpt/test_expr_complex.c
index 2ae412b5..ea2d8e52 100644
--- a/test/ArrayOpt/test_expr_complex.c
+++ b/test/ArrayOpt/test_expr_complex.c
@@ -4,8 +4,23 @@
 // RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I
 // RUN: test -f %t.klee-out/test000001.kquery
 // RUN: test -f %t.klee-out/test000002.kquery
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=value %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V
+// RUN: test -f %t.klee-out/test000001.kquery
+// RUN: test -f %t.klee-out/test000002.kquery
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=all %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I
+// RUN: test -f %t.klee-out/test000001.kquery
+// RUN: test -f %t.klee-out/test000002.kquery
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
 
 // CHECK-OPT_I: KLEE: WARNING: OPT_I: successful
+// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful
 // CHECK-CONST_ARR: const_arr
 
 #include <stdio.h>
diff --git a/test/ArrayOpt/test_expr_simple.c b/test/ArrayOpt/test_expr_simple.c
index 433b864f..53af9a2b 100644
--- a/test/ArrayOpt/test_expr_simple.c
+++ b/test/ArrayOpt/test_expr_simple.c
@@ -4,8 +4,23 @@
 // RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I
 // RUN: test -f %t.klee-out/test000001.kquery
 // RUN: test -f %t.klee-out/test000002.kquery
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=value %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V
+// RUN: test -f %t.klee-out/test000001.kquery
+// RUN: test -f %t.klee-out/test000002.kquery
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=all %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I
+// RUN: test -f %t.klee-out/test000001.kquery
+// RUN: test -f %t.klee-out/test000002.kquery
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
 
 // CHECK-OPT_I: KLEE: WARNING: OPT_I: successful
+// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful
 // CHECK-CONST_ARR: const_arr
 
 #include <stdio.h>
diff --git a/test/ArrayOpt/test_feasible.c b/test/ArrayOpt/test_feasible.c
index 17bfa523..1bbb341b 100644
--- a/test/ArrayOpt/test_feasible.c
+++ b/test/ArrayOpt/test_feasible.c
@@ -6,8 +6,23 @@
 // RUN: test -f %t.klee-out/test000002.kquery
 // RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
 // RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=value %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V
+// RUN: test -f %t.klee-out/test000001.kquery
+// RUN: test -f %t.klee-out/test000002.kquery
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=all %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I
+// RUN: test -f %t.klee-out/test000001.kquery
+// RUN: test -f %t.klee-out/test000002.kquery
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
 
 // CHECK-OPT_I: KLEE: WARNING: OPT_I: successful
+// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful
 // CHECK-CONST_ARR: const_arr
 
 #include <stdio.h>
diff --git a/test/ArrayOpt/test_multindex.c b/test/ArrayOpt/test_multindex.c
index 4dada79d..91519466 100644
--- a/test/ArrayOpt/test_multindex.c
+++ b/test/ArrayOpt/test_multindex.c
@@ -2,8 +2,23 @@
 // 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
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=value %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V
+// RUN: test -f %t.klee-out/test000001.kquery
+// RUN: test -f %t.klee-out/test000002.kquery
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=all %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V
+// RUN: test -f %t.klee-out/test000001.kquery
+// RUN: test -f %t.klee-out/test000002.kquery
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
 
 // CHECK-OPT_I: KLEE: WARNING: OPT_I: successful
+// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful
 // CHECK-CONST_ARR: const_arr
 
 #include <stdio.h>
diff --git a/test/ArrayOpt/test_new.c b/test/ArrayOpt/test_new.c
index 7e095e76..8a66d1f6 100644
--- a/test/ArrayOpt/test_new.c
+++ b/test/ArrayOpt/test_new.c
@@ -4,8 +4,23 @@
 // RUN: not FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I
 // RUN: test -f %t.klee-out/test000001.kquery
 // RUN: test -f %t.klee-out/test000002.kquery
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=value %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V
+// RUN: test -f %t.klee-out/test000001.kquery
+// RUN: test -f %t.klee-out/test000002.kquery
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=all %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V
+// RUN: test -f %t.klee-out/test000001.kquery
+// RUN: test -f %t.klee-out/test000002.kquery
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
 
 // CHECK-OPT_I: KLEE: WARNING: OPT_I: successful
+// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful
 // CHECK-CONST_ARR: const_arr
 
 #include <stdio.h>
diff --git a/test/ArrayOpt/test_nier.c b/test/ArrayOpt/test_nier.c
index 93fb96aa..40e36a3d 100644
--- a/test/ArrayOpt/test_nier.c
+++ b/test/ArrayOpt/test_nier.c
@@ -6,8 +6,23 @@
 // RUN: test -f %t.klee-out/test000002.kquery
 // RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
 // RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=value %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V
+// RUN: test -f %t.klee-out/test000001.kquery
+// RUN: test -f %t.klee-out/test000002.kquery
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=all %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I
+// RUN: test -f %t.klee-out/test000001.kquery
+// RUN: test -f %t.klee-out/test000002.kquery
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
 
 // CHECK-OPT_I: KLEE: WARNING: OPT_I: successful
+// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful
 // CHECK-CONST_ARR: const_arr
 
 #include<stdio.h>
diff --git a/test/ArrayOpt/test_noncontiguous_idx.c b/test/ArrayOpt/test_noncontiguous_idx.c
index 8eb16021..380c3aea 100644
--- a/test/ArrayOpt/test_noncontiguous_idx.c
+++ b/test/ArrayOpt/test_noncontiguous_idx.c
@@ -4,10 +4,26 @@
 // RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I
 // RUN: test -f %t.klee-out/test000001.kquery
 // RUN: test -f %t.klee-out/test000002.kquery
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=value %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V
+// RUN: test -f %t.klee-out/test000001.kquery
+// RUN: test -f %t.klee-out/test000002.kquery
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=all %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I
+// RUN: test -f %t.klee-out/test000001.kquery
+// RUN: test -f %t.klee-out/test000002.kquery
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
 
 // CHECK-OPT_I: KLEE: WARNING: OPT_I: successful
+// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful
 // CHECK-CONST_ARR: const_arr
 
+
 #include <stdio.h>
 #include "klee/klee.h"
 
diff --git a/test/ArrayOpt/test_position.c b/test/ArrayOpt/test_position.c
index e42371b6..fcf5aeaa 100644
--- a/test/ArrayOpt/test_position.c
+++ b/test/ArrayOpt/test_position.c
@@ -4,8 +4,23 @@
 // RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I
 // RUN: test -f %t.klee-out/test000001.kquery
 // RUN: test -f %t.klee-out/test000002.kquery
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=value %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V
+// RUN: test -f %t.klee-out/test000001.kquery
+// RUN: test -f %t.klee-out/test000002.kquery
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=all %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I
+// RUN: test -f %t.klee-out/test000001.kquery
+// RUN: test -f %t.klee-out/test000002.kquery
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
 
 // CHECK-OPT_I: KLEE: WARNING: OPT_I: successful
+// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful
 // CHECK-CONST_ARR: const_arr
 
 #include <stdio.h>
diff --git a/test/ArrayOpt/test_sub_idx.c b/test/ArrayOpt/test_sub_idx.c
index ef068427..34201274 100644
--- a/test/ArrayOpt/test_sub_idx.c
+++ b/test/ArrayOpt/test_sub_idx.c
@@ -6,8 +6,23 @@
 // RUN: test -f %t.klee-out/test000002.kquery
 // RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
 // RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=value %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V
+// RUN: test -f %t.klee-out/test000001.kquery
+// RUN: test -f %t.klee-out/test000002.kquery
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=all %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I
+// RUN: test -f %t.klee-out/test000001.kquery
+// RUN: test -f %t.klee-out/test000002.kquery
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
 
 // CHECK-OPT_I: KLEE: WARNING: OPT_I: successful
+// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful
 // CHECK-CONST_ARR: const_arr
 
 #include <stdio.h>
diff --git a/test/ArrayOpt/test_var_idx.c b/test/ArrayOpt/test_var_idx.c
index 4fbfe7ce..e9f159c1 100644
--- a/test/ArrayOpt/test_var_idx.c
+++ b/test/ArrayOpt/test_var_idx.c
@@ -6,8 +6,23 @@
 // RUN: test -f %t.klee-out/test000002.kquery
 // RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
 // RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=value %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V
+// RUN: test -f %t.klee-out/test000001.kquery
+// RUN: test -f %t.klee-out/test000002.kquery
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=all %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I
+// RUN: test -f %t.klee-out/test000001.kquery
+// RUN: test -f %t.klee-out/test000002.kquery
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
 
 // CHECK-OPT_I: KLEE: WARNING: OPT_I: successful
+// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful
 // CHECK-CONST_ARR: const_arr
 
 #include <stdio.h>

 

generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-06-03 04:11:33 +0000