blob: 71f0288f076e6c1bd09d1f90dcb5fcfd13e0c283 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
# RUN: %kleaver -print-ast -pc-multibyte-reads=true %s > %t.log
# RUN: grep -q "(ReadLSB w32 4 arr1)" %t.log
# RUN: grep -q "(ReadMSB w32 2 arr2)" %t.log
array arr1[8] : w32 -> w8 = symbolic
array arr2[8] : w32 -> w8 = symbolic
(query [(Not (Slt 100
(Concat w32 (Read w8 7 arr1)
(Concat w24 (Read w8 6 arr1)
(Concat w16 (Read w8 5 arr1) (Read w8 4 arr1))))))]
false)
(query [(Not (Slt 100
(Concat w32 (Read w8 2 arr2)
(Concat w24 (Read w8 3 arr2)
(Concat w16 (Read w8 4 arr2) (Read w8 5 arr2))))))]
false)
|
