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:
8 Unable to resolve constraint:
10 needed to satisfy precondition:
11 requires maxSet(x @ sizeof.c:17:1) >= 3
12 test3.c:2:6: Function t defined more than once
13 m.c:11:1: Previous definition of t
14 test3.c: (in function t)
15 test3.c:9:3: Likely out-of-bounds store:
17 Unable to resolve constraint:
19 needed to satisfy precondition:
20 requires maxSet(g @ test3.c:9:3) >= 101
21 test7.c:2:6: Function t defined more than once
22 m.c:11:1: Previous definition of t
23 test7.c: (in function t)
24 test7.c:6:3: Possible out-of-bounds store:
26 Unable to resolve constraint:
27 requires maxSet(g @ test7.c:4:3) >= 4
28 needed to satisfy precondition:
29 requires maxSet(g @ test7.c:6:3) >= 2
30 test7.c:8:3: Possible out-of-bounds store:
32 Unable to resolve constraint:
33 requires maxSet(j @ test7.c:8:3) >= 0
34 needed to satisfy precondition:
35 requires maxSet(j @ test7.c:8:3) >= 0
37 Finished checking --- 7 code warnings, as expected