about summary refs log tree commit diff homepage
path: root/test/Feature
diff options
context:
space:
mode:
authorEric Rizzi <eric.rizzi@gmail.com>2015-09-14 14:32:37 -0400
committerDan Liew <delcypher@gmail.com>2016-11-23 20:36:44 +0000
commitf27cf86466d75c71a302abe5e0a3ffcad1670373 (patch)
treedd598d703d01fc8292afa6cc56816ec822715923 /test/Feature
parent094a21832d94bfaa5da8ea667e646328ca0e5432 (diff)
downloadklee-f27cf86466d75c71a302abe5e0a3ffcad1670373.tar.gz
Renamed .pc to .kquery (kleaver query)
Diffstat (limited to 'test/Feature')
-rw-r--r--test/Feature/CompressedExprLogging.c8
-rw-r--r--test/Feature/ExprLogging.c6
-rw-r--r--test/Feature/MultiMkSym.c4
-rw-r--r--test/Feature/RewriteEqualities.c10
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>