diff options
| author | Timotej Kapus <timotej.kapus13@imperial.ac.uk> | 2018-03-16 10:42:12 +0000 |
|---|---|---|
| committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2018-05-09 12:19:53 +0100 |
| commit | 13b5bcbfd933461526f08c6ad759af9e129d6764 (patch) | |
| tree | fb3eb848493ccf697f8193aeae81d098874dc340 /test/Solver/Z3ConstantArray.c | |
| parent | e0aff85c24c039606d82d209617a1334a9ed21e2 (diff) | |
| download | klee-13b5bcbfd933461526f08c6ad759af9e129d6764.tar.gz | |
Improve handling of constant array in Z3
Diffstat (limited to 'test/Solver/Z3ConstantArray.c')
| -rw-r--r-- | test/Solver/Z3ConstantArray.c | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/test/Solver/Z3ConstantArray.c b/test/Solver/Z3ConstantArray.c new file mode 100644 index 00000000..482679e9 --- /dev/null +++ b/test/Solver/Z3ConstantArray.c @@ -0,0 +1,28 @@ +// REQUIRES: z3 +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out -solver-backend=z3 -write-cvcs -write-smt2s -debug-z3-dump-queries=%t.smt2 %t1.bc +// RUN: cat %t.klee-out/test000001.smt2 | FileCheck --check-prefix=TEST-CASE %s +// RUN: cat %t.klee-out/test000002.smt2 | FileCheck --check-prefix=TEST-CASE %s +// RUN: cat %t.smt2 | FileCheck %s + +#include "klee/klee.h" + +int main(int argc, char **argv) { + // CHECK-DAG: (assert (= (select const_arr11 #x00000000) #x67)) + // CHECK-DAG: (assert (= (select const_arr11 #x00000001) #x79)) + // CHECK-DAG: (assert (= (select const_arr11 #x00000002) #x7a)) + // CHECK-DAG: (assert (= (select const_arr11 #x00000003) #x00)) + // TEST-CASE-DAG: (assert (= (select const_arr1 (_ bv0 32) ) (_ bv103 8) ) ) + // TEST-CASE-DAG: (assert (= (select const_arr1 (_ bv1 32) ) (_ bv121 8) ) ) + // TEST-CASE-DAG: (assert (= (select const_arr1 (_ bv2 32) ) (_ bv122 8) ) ) + // TEST-CASE-DAG: (assert (= (select const_arr1 (_ bv3 32) ) (_ bv0 8) ) ) + char c[4] = {'g', 'y', 'z', '\0'}; + unsigned i; + klee_make_symbolic(&i, sizeof i, "i"); + klee_assume(i < 4); + if (c[i] < 'y') + return 0; + else + return 1; +} |