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))]
+sizeof.c:17:1: Likely out-of-bounds store: x[(sizeof(x))]
Unable to resolve constraint:
requires 2 >= 3
needed to satisfy precondition:
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]
+test3.c:9:3: Likely out-of-bounds store: g[101]
Unable to resolve constraint:
requires 99 >= 101
needed to satisfy precondition:
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]
+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]
+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: