about summary refs log tree commit diff homepage
path: root/test/Expr
diff options
context:
space:
mode:
Diffstat (limited to 'test/Expr')
-rw-r--r--test/Expr/Evaluate.kquery (renamed from test/Expr/Evaluate.pc)0
-rw-r--r--test/Expr/Evaluate2.kquery (renamed from test/Expr/Evaluate2.pc)0
-rw-r--r--test/Expr/Lexer/Numbers.kquery (renamed from test/Expr/Lexer/Numbers.pc)0
-rw-r--r--test/Expr/Parser/Concat64.kquery (renamed from test/Expr/Parser/Concat64.pc)0
-rw-r--r--test/Expr/Parser/ConstantFolding.kquery (renamed from test/Expr/Parser/ConstantFolding.pc)0
-rw-r--r--test/Expr/Parser/Exprs.kquery (renamed from test/Expr/Parser/Exprs.pc)0
-rw-r--r--test/Expr/Parser/MultiByteReads.kquery (renamed from test/Expr/Parser/MultiByteReads.pc)0
-rw-r--r--test/Expr/Parser/Simplify.kquery (renamed from test/Expr/Parser/Simplify.pc)0
-rw-r--r--test/Expr/Parser/TypeChecking.kquery16
-rw-r--r--test/Expr/Parser/TypeChecking.pc16
-rw-r--r--test/Expr/print-smt-let.kquery (renamed from test/Expr/print-smt-let.pc)0
-rw-r--r--test/Expr/print-smt-named.kquery (renamed from test/Expr/print-smt-named.pc)0
-rw-r--r--test/Expr/print-smt-none.kquery (renamed from test/Expr/print-smt-none.pc)0
13 files changed, 16 insertions, 16 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