Renamed .pc to .kquery (kleaver query)

20 files changed, 31 insertions, 31 deletions

diff --git a/test/Expr/Evaluate.pc b/test/Expr/Evaluate.kquery
index 43134475..43134475 100644
--- a/test/Expr/Evaluate.pc
+++ b/test/Expr/Evaluate.kquery
diff --git a/test/Expr/Evaluate2.pc b/test/Expr/Evaluate2.kquery
index d62241f0..d62241f0 100644
--- a/test/Expr/Evaluate2.pc
+++ b/test/Expr/Evaluate2.kquery
diff --git a/test/Expr/Lexer/Numbers.pc b/test/Expr/Lexer/Numbers.kquery
index 6b8e2e37..6b8e2e37 100644
--- a/test/Expr/Lexer/Numbers.pc
+++ b/test/Expr/Lexer/Numbers.kquery
diff --git a/test/Expr/Parser/Concat64.pc b/test/Expr/Parser/Concat64.kquery
index 0b1479d4..0b1479d4 100644
--- a/test/Expr/Parser/Concat64.pc
+++ b/test/Expr/Parser/Concat64.kquery
diff --git a/test/Expr/Parser/ConstantFolding.pc b/test/Expr/Parser/ConstantFolding.kquery
index a02920db..a02920db 100644
--- a/test/Expr/Parser/ConstantFolding.pc
+++ b/test/Expr/Parser/ConstantFolding.kquery
diff --git a/test/Expr/Parser/Exprs.pc b/test/Expr/Parser/Exprs.kquery
index 4a6adf7e..4a6adf7e 100644
--- a/test/Expr/Parser/Exprs.pc
+++ b/test/Expr/Parser/Exprs.kquery
diff --git a/test/Expr/Parser/MultiByteReads.pc b/test/Expr/Parser/MultiByteReads.kquery
index 71f0288f..71f0288f 100644
--- a/test/Expr/Parser/MultiByteReads.pc
+++ b/test/Expr/Parser/MultiByteReads.kquery
diff --git a/test/Expr/Parser/Simplify.pc b/test/Expr/Parser/Simplify.kquery
index 6d817b6f..6d817b6f 100644
--- a/test/Expr/Parser/Simplify.pc
+++ b/test/Expr/Parser/Simplify.kquery
diff --git a/test/Expr/Parser/TypeChecking.kquery b/test/Expr/Parser/TypeChecking.kquery
new file mode 100644
index 00000000..d9685b70
--- /dev/null
+++ b/test/Expr/Parser/TypeChecking.kquery
@@ -0,0 +1,16 @@
+# RUN: not %kleaver %s 2> %t.log
+
+
+
+# RUN: grep "TypeChecking.kquery:7:9: error: type widths do not match in binary expression" %t.log
+array arr1[8] : w32 -> w8 = symbolic
+(query [(Eq (ReadLSB w32 0 arr1) true)]
+       false)
+
+# RUN: grep "TypeChecking.kquery:14:25: error: invalid write index (doesn't match array domain)" %t.log
+# RUN: grep "TypeChecking.kquery:14:35: error: invalid write value (doesn't match array range)" %t.log
+# FIXME: Add array declarations
+array arr2[8] : w32 -> w8 = symbolic
+(query [(Eq (Read w8 0 [ (w17 0) = (w9 0) ] @ arr2) 0)] false)
+
+# RUN: grep "TypeChecking.kquery: parse failure: 3 errors." %t.log
diff --git a/test/Expr/Parser/TypeChecking.pc b/test/Expr/Parser/TypeChecking.pc
deleted file mode 100644
index 66991c20..00000000
--- a/test/Expr/Parser/TypeChecking.pc
+++ /dev/null
@@ -1,16 +0,0 @@
-# RUN: not %kleaver %s 2> %t.log
-
-
-
-# RUN: grep "TypeChecking.pc:7:9: error: type widths do not match in binary expression" %t.log
-array arr1[8] : w32 -> w8 = symbolic
-(query [(Eq (ReadLSB w32 0 arr1) true)] 
-       false)
-
-# RUN: grep "TypeChecking.pc:14:25: error: invalid write index (doesn't match array domain)" %t.log
-# RUN: grep "TypeChecking.pc:14:35: error: invalid write value (doesn't match array range)" %t.log
-# FIXME: Add array declarations
-array arr2[8] : w32 -> w8 = symbolic
-(query [(Eq (Read w8 0 [ (w17 0) = (w9 0) ] @ arr2) 0)] false)
-
-# RUN: grep "TypeChecking.pc: parse failure: 3 errors." %t.log
diff --git a/test/Expr/print-smt-let.pc b/test/Expr/print-smt-let.kquery
index de097135..de097135 100644
--- a/test/Expr/print-smt-let.pc
+++ b/test/Expr/print-smt-let.kquery
diff --git a/test/Expr/print-smt-named.pc b/test/Expr/print-smt-named.kquery
index 0e0d87b7..0e0d87b7 100644
--- a/test/Expr/print-smt-named.pc
+++ b/test/Expr/print-smt-named.kquery
diff --git a/test/Expr/print-smt-none.pc b/test/Expr/print-smt-none.kquery
index c29392ab..c29392ab 100644
--- a/test/Expr/print-smt-none.pc
+++ b/test/Expr/print-smt-none.kquery
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>
diff --git a/test/Solver/FastCexSolver.pc b/test/Solver/FastCexSolver.kquery
index b3ec63e3..b3ec63e3 100644
--- a/test/Solver/FastCexSolver.pc
+++ b/test/Solver/FastCexSolver.kquery
diff --git a/test/Solver/LargeIntegers.pc b/test/Solver/LargeIntegers.kquery
index e0921393..e0921393 100644
--- a/test/Solver/LargeIntegers.pc
+++ b/test/Solver/LargeIntegers.kquery
diff --git a/test/lit.cfg b/test/lit.cfg
index fdf9bf7b..4fe24ba2 100644
--- a/test/lit.cfg
+++ b/test/lit.cfg
@@ -21,7 +21,7 @@ config.test_format = lit.formats.ShTest(execute_external=False)
 
 # suffixes: A list of file extensions to treat as test files
 # Note this can be overridden by lit.local.cfg files
-config.suffixes = ['.ll', '.c', '.cpp', '.pc']
+config.suffixes = ['.ll', '.c', '.cpp', '.kquery']
 
 # test_source_root: The root path where tests are located.
 config.test_source_root = os.path.dirname(__file__)