unrecogCall.c:8:3: Unrecognized identifier: bar
initialization.c: (in function initialization)
initialization.c:5:10: Variable g declared but not used
-initialization.c:5:14: Possible out-of-bounds read:
- e[22]
+initialization.c:5:14: Possible out-of-bounds read: e[22]
Unable to resolve constraint:
requires maxRead(d @ initialization.c:3:14) >= 22
needed to satisfy precondition:
requires maxRead(e @ initialization.c:5:14) >= 22
-initialization.c:8:3: Possible out-of-bounds store:
- f[2]
+initialization.c:8:3: Possible out-of-bounds store: f[2]
Unable to resolve constraint:
requires maxSet(d @ initialization.c:3:14) >= 2
needed to satisfy precondition:
requires maxSet(f @ initialization.c:8:3) >= 2
simplifyTest.c: (in function fooSub)
-simplifyTest.c:3:3: Possible out-of-bounds store:
- s[i]
+simplifyTest.c:3:3: Possible out-of-bounds store: s[i]
Unable to resolve constraint:
requires maxSet(s @ simplifyTest.c:3:3) >= i @ simplifyTest.c:3:5
needed to satisfy precondition:
requires maxSet(s @ simplifyTest.c:3:3) >= i @ simplifyTest.c:3:5
simplifyTest.c: (in function fooAdd)
-simplifyTest.c:10:3: Possible out-of-bounds store:
- s[i + 2]
+simplifyTest.c:10:3: Possible out-of-bounds store: s[i + 2]
Unable to resolve constraint:
requires maxSet(s @ simplifyTest.c:10:3) >= i @ simplifyTest.c:10:5 + 2
needed to satisfy precondition: