blob: 9d0d272cd4ffe432d09cfb04e1ae4a7039b390c0 (
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 left overshift to zero when shifting a constant ALWAYS!
(query [ (Ule (w32 32) (ReadLSB w32 (w32 0) shift)) ]
(Eq
(Shl 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
(Shl w64 (w64 2)
(ReadLSB w64 (w32 0) shift64)
)
(w64 0)
) [ ] [shift64] )
|
