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