blob: af563ea3adf2f4bdd5c0ccfc5b2357863bf9e003 (
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 → ( ( ( (signed int)2 ) >> x) = 0 )
# Check we arithmetic right overshift to zero when shifting a constant ALWAYS!
(query [ (Ule (w32 32) (ReadLSB w32 (w32 0) shift)) ]
(Eq
(AShr w32 (w32 2)
(ReadLSB w32 (w32 0) shift)
)
(w32 0)
) [ ] [shift] )
# 64-bit version
# ∀ x. x >= 64 → ( (((signed int) 2) >> x) = 0 )
array shift64[8] : w32 -> w8 = symbolic
(query [ (Ule (w64 64) (ReadLSB w64 (w32 0) shift64)) ]
(Eq
(AShr w64 (w64 2)
(ReadLSB w64 (w32 0) shift64)
)
(w64 0)
) [ ] [shift64] )
|
