blob: 43134475257e8b138c4e35a0c12c89925df4266d (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
# RUN: %kleaver -evaluate %s > %t.log
array arr0[4] : w32 -> w8 = symbolic
array arr1[8] : w32 -> w8 = symbolic
# RUN: grep "Query 0: INVALID" %t.log
# Query 0
(query [] (Not (Ult (ReadLSB w32 0 arr0)
16)))
# RUN: grep "Query 1: VALID" %t.log
# Query 1
(query [(Eq N0:(ReadLSB w32 0 arr1) 10)
(Eq N1:(ReadLSB w32 4 arr1) 20)]
(Eq (Add w32 N0 N1)
30))
# RUN: grep "Query 2: VALID" %t.log
# Query 2
array hello[4] : w32 -> w8 = [ 1 2 3 5 ]
(query [] (Eq (Add w8 (Read w8 0 hello)
(Read w8 3 hello))
6))
# RUN: grep "Query 3: VALID" %t.log
# Query 2
(query [] (Eq (Not w8 (Read w8 0 arr1))
(Xor w8 (Read w8 0 arr1) 0xff)))
|
