blob: d9685b70d2fef78a5d4b053fa342925714f40c45 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
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
|
