m.c: (in function t)
m.c:9:1: Index of possibly null pointer f: f
   m.c:8:5: Storage f may become null
sizeof.c: (in function f)
sizeof.c:17:1: Likely out-of-bounds store:
    x[(sizeof(x))]
    Unable to resolve constraint:
    requires 2 >= 3
     needed to satisfy precondition:
    requires maxSet(x @ sizeof.c:17:1) >= 3
test3.c:2:6: Function t defined more than once
   m.c:11:1: Previous definition of t
test3.c: (in function t)
test3.c:9:3: Likely out-of-bounds store:
    g[101]
    Unable to resolve constraint:
    requires 99 >= 101
     needed to satisfy precondition:
    requires maxSet(g @ test3.c:9:3) >= 101
test7.c:2:6: Function t defined more than once
   m.c:11:1: Previous definition of t
test7.c: (in function t)
test7.c:6:3: Possible out-of-bounds store:
    g[2]
    Unable to resolve constraint:
    requires maxSet(g @ test7.c:4:3) >= 4
     needed to satisfy precondition:
    requires maxSet(g @ test7.c:6:3) >= 2
test7.c:8:3: Possible out-of-bounds store:
    j[0]
    Unable to resolve constraint:
    requires maxSet(j @ test7.c:8:3) >= 0
     needed to satisfy precondition:
    requires maxSet(j @ test7.c:8:3) >= 0

Finished checking --- 7 code warnings, as expected