-simplifyTest.c:10:3: Unresolved constraint:
- Lclint is unable to resolve Requires: : MAXSET ((s @ simplifyTest.c:10:3 )
- ) >= ((i @ simplifyTest.c:10:5 ) ) + (( 2 ) ) needed to satisfy Requires:
- : MAXSET ((s @ simplifyTest.c:10:3 ) ) >= ((i @ simplifyTest.c:10:5 ) ) +
- (( 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:
+ requires maxSet(s @ simplifyTest.c:10:3) >= i @ simplifyTest.c:10:5 + 2
+strncatNotReallyGood.c: (in function NotGoodfunc)
+strncatNotReallyGood.c:4:29: Passed storage buffer not completely defined
+ (*buffer is undefined): strncat (buffer, ...)
+strncatNotReallyGood.c:4:21: Possible out-of-bounds store:
+ strncat(buffer, str, sizeof((buffer)) - 1)
+ Unable to resolve constraint:
+ requires maxRead(buffer @ strncatNotReallyGood.c:4:29) <= 0
+ needed to satisfy precondition:
+ requires maxSet(buffer @ strncatNotReallyGood.c:4:29) >= maxRead(buffer @
+ strncatNotReallyGood.c:4:29) + 255
+ derived from strncat precondition: requires maxSet(<parameter 1>) >=
+ maxRead(<parameter 1>) + <parameter 3>