diff options
author | Eric Rizzi <eric.rizzi@gmail.com> | 2015-09-14 14:32:37 -0400 |
---|---|---|
committer | Dan Liew <delcypher@gmail.com> | 2016-11-23 20:36:44 +0000 |
commit | f27cf86466d75c71a302abe5e0a3ffcad1670373 (patch) | |
tree | dd598d703d01fc8292afa6cc56816ec822715923 /test/Expr | |
parent | 094a21832d94bfaa5da8ea667e646328ca0e5432 (diff) | |
download | klee-f27cf86466d75c71a302abe5e0a3ffcad1670373.tar.gz |
Renamed .pc to .kquery (kleaver query)
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.kquery | 16 | ||||
-rw-r--r-- | test/Expr/Parser/TypeChecking.pc | 16 | ||||
-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 |