blob: d2deabbec847724cdcc970ab15cd0bdf9487146e (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
# RUN: %kleaver %s 2>&1 | FileCheck %s
array n_args[4] : w32 -> w8 = symbolic
array n_args_1[4] : w32 -> w8 = symbolic
array A_data_stat[144] : w32 -> w8 = symbolic
array stdin_stat[144] : w32 -> w8 = symbolic
(query [(Ult N0:(ReadLSB w32 0 n_args) 2)
(Slt 0 N0)
(Ult N1:(ReadLSB w32 0 n_args_1) 3)
(Slt 0 N1)
(Slt 1 N1)
(Eq false (Eq 0 (And w64 (ReadLSB w64 8 A_data_stat) 2147483647)))
(Ult (ReadLSB w64 56 A_data_stat) 65536)
(Eq false (Eq 0 (And w64 (ReadLSB w64 8 stdin_stat) 2147483647)))]
(Eq false (Ult (ReadLSB w64 56 stdin_stat) 65536)) [] [n_args])
# CHECK: INVALID
|
