diff options
Diffstat (limited to 'test/Feature')
-rw-r--r-- | test/Feature/CompressedExprLogging.c | 8 | ||||
-rw-r--r-- | test/Feature/ExprLogging.c | 6 | ||||
-rw-r--r-- | test/Feature/MultiMkSym.c | 4 | ||||
-rw-r--r-- | test/Feature/RewriteEqualities.c | 10 |
4 files changed, 14 insertions, 14 deletions
diff --git a/test/Feature/CompressedExprLogging.c b/test/Feature/CompressedExprLogging.c index a2a07d8b..425c4551 100644 --- a/test/Feature/CompressedExprLogging.c +++ b/test/Feature/CompressedExprLogging.c @@ -3,10 +3,10 @@ // solvers, in particular when counting the number of queries in the last two // commands // RUN: rm -rf %t.klee-out %t.klee-out2 -// RUN: %klee --output-dir=%t.klee-out --use-cex-cache=false --use-query-log=all:pc %t1.bc -// RUN: %klee --output-dir=%t.klee-out2 --use-cex-cache=false --compress-query-log --use-query-log=all:pc %t1.bc -// RUN: gunzip -d %t.klee-out2/all-queries.pc.gz -// RUN: diff %t.klee-out/all-queries.pc %t.klee-out/all-queries.pc +// RUN: %klee --output-dir=%t.klee-out --use-cex-cache=false --use-query-log=all:kquery %t1.bc +// RUN: %klee --output-dir=%t.klee-out2 --use-cex-cache=false --compress-query-log --use-query-log=all:kquery %t1.bc +// RUN: gunzip -d %t.klee-out2/all-queries.kquery.gz +// RUN: diff %t.klee-out/all-queries.kquery %t.klee-out/all-queries.kquery #include <assert.h> diff --git a/test/Feature/ExprLogging.c b/test/Feature/ExprLogging.c index bba0570e..4479e850 100644 --- a/test/Feature/ExprLogging.c +++ b/test/Feature/ExprLogging.c @@ -1,11 +1,11 @@ // RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t1.bc // We disable the cex-cache to eliminate nondeterminism across different solvers, in particular when counting the number of queries in the last two commands // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --use-cex-cache=false --use-query-log=all:pc,all:smt2,solver:pc,solver:smt2 --write-pcs --write-cvcs --write-smt2s %t1.bc 2> %t2.log -// RUN: %kleaver -print-ast %t.klee-out/all-queries.pc > %t3.log +// RUN: %klee --output-dir=%t.klee-out --use-cex-cache=false --use-query-log=all:kquery,all:smt2,solver:kquery,solver:smt2 --write-kqueries --write-cvcs --write-smt2s %t1.bc 2> %t2.log +// RUN: %kleaver -print-ast %t.klee-out/all-queries.kquery > %t3.log // RUN: %kleaver -print-ast %t3.log > %t4.log // RUN: diff %t3.log %t4.log -// RUN: %kleaver -print-ast %t.klee-out/solver-queries.pc > %t3.log +// RUN: %kleaver -print-ast %t.klee-out/solver-queries.kquery > %t3.log // RUN: %kleaver -print-ast %t3.log > %t4.log // RUN: diff %t3.log %t4.log // RUN: grep "^; Query" %t.klee-out/all-queries.smt2 | wc -l | grep -q 17 diff --git a/test/Feature/MultiMkSym.c b/test/Feature/MultiMkSym.c index 85b6ed70..fde864d7 100644 --- a/test/Feature/MultiMkSym.c +++ b/test/Feature/MultiMkSym.c @@ -1,7 +1,7 @@ // RUN: %llvmgcc -I../../../include -emit-llvm -g -c %s -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --write-pcs %t.bc > %t.log -// RUN: cat %t.klee-out/test000001.pc %t.klee-out/test000002.pc %t.klee-out/test000003.pc %t.klee-out/test000004.pc > %t1 +// RUN: %klee --output-dir=%t.klee-out --write-kqueries %t.bc > %t.log +// RUN: cat %t.klee-out/test000001.kquery %t.klee-out/test000002.kquery %t.klee-out/test000003.kquery %t.klee-out/test000004.kquery > %t1 // RUN: grep "a\[1\]" %t1 | wc -l | grep 2 // RUN: grep "a\[100\]" %t1 | wc -l | grep 2 diff --git a/test/Feature/RewriteEqualities.c b/test/Feature/RewriteEqualities.c index 3cb9c5fe..6bf199f7 100644 --- a/test/Feature/RewriteEqualities.c +++ b/test/Feature/RewriteEqualities.c @@ -1,11 +1,11 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --search=dfs --write-pcs --rewrite-equalities=false %t.bc -// RUN: grep "N0:(Read w8 2 x)" %t.klee-out/test000003.pc -// RUN: grep "N0)" %t.klee-out/test000003.pc +// RUN: %klee --output-dir=%t.klee-out --search=dfs --write-kqueries --rewrite-equalities=false %t.bc +// RUN: grep "N0:(Read w8 2 x)" %t.klee-out/test000003.kquery +// RUN: grep "N0)" %t.klee-out/test000003.kquery // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --search=dfs --write-pcs --rewrite-equalities %t.bc -// RUN: grep "(Read w8 8 const_arr1)" %t.klee-out/test000003.pc +// RUN: %klee --output-dir=%t.klee-out --search=dfs --write-kqueries --rewrite-equalities %t.bc +// RUN: grep "(Read w8 8 const_arr1)" %t.klee-out/test000003.kquery #include <stdio.h> #include <klee/klee.h> |