blob: 7ca6d4d58ac1842fe5ade28c9a639e9ffeead674 (
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
|
# RUN: %kleaver %s > %t
# RUN: not grep INVALID %t
array shift[4] : w32 -> w8 = symbolic
# ∀ x. x >= 32 → ( (2 >> x) = 0 )
# Check we logical right overshift to zero when shifting a constant ALWAYS!
(query [ (Ule (w32 32) (ReadLSB w32 (w32 0) shift)) ]
(Eq
(LShr w32 (w32 2)
(ReadLSB w32 (w32 0) shift)
)
(w32 0)
) [ ] [shift] )
# 64-bit version
# ∀ x. x >= 64 → ( (2 >> x) = 0 )
array shift64[8] : w32 -> w8 = symbolic
(query [ (Ule (w64 64) (ReadLSB w64 (w32 0) shift64)) ]
(Eq
(LShr w64 (w64 2)
(ReadLSB w64 (w32 0) shift64)
)
(w64 0)
) [ ] [shift64] )
|
