3 m.c:9:1: Index of possibly null pointer f: f
4 m.c:8:5: Storage f may become null
5 sizeof.c: (in function f)
6 sizeof.c:17:1: Likely out-of-bounds store: x[(sizeof(x))]
7 Unable to resolve constraint:
9 needed to satisfy precondition:
10 requires maxSet(x @ sizeof.c:17:1) >= 3
11 test3.c:2:6: Function t defined more than once
12 m.c:11:1: Previous definition of t
13 test3.c: (in function t)
14 test3.c:9:3: Likely out-of-bounds store: g[101]
15 Unable to resolve constraint:
17 needed to satisfy precondition:
18 requires maxSet(g @ test3.c:9:3) >= 101
19 test7.c:2:6: Function t defined more than once
20 m.c:11:1: Previous definition of t
21 test7.c: (in function t)
22 test7.c:6:3: Possible out-of-bounds store: g[2]
23 Unable to resolve constraint:
24 requires maxSet(g @ test7.c:4:3) >= 4
25 needed to satisfy precondition:
26 requires maxSet(g @ test7.c:6:3) >= 2
27 test7.c:8:3: Possible out-of-bounds store: j[0]
28 Unable to resolve constraint:
29 requires maxSet(j @ test7.c:8:3) >= 0
30 needed to satisfy precondition:
31 requires maxSet(j @ test7.c:8:3) >= 0
33 Finished checking --- 7 code warnings, as expected