undefined): mystrncat (buffer, ...)
mystrncat.c:13:13: Passed storage b not completely defined (*b is undefined):
mystrncat (b, ...)
-mystrncat.c:13:3: Possible out-of-bounds store. Unable to resolve constraint:
- requires: : maxRead ((malloc(256) @ mystrncat.c:10:7 ) ) <= ( 0 )
+ mystrncat.c:10:3: Storage *b allocated
+mystrncat.c:12:3: Possible out-of-bounds store:
+ mystrncat(buffer, str, sizeof((buffer)) - 1)
+ Unable to resolve constraint:
+ requires maxRead(buffer @ mystrncat.c:12:13) <= 0
needed to satisfy precondition:
- requires: : maxSet ((b @ mystrncat.c:13:13 ) ) >= (maxRead ((b @
- mystrncat.c:13:13 ) )) + (( 255 ) )
- derived from mystrncat precondition: requires: :
- maxSet ((<parameter 1> ) ) >= (maxRead ((<parameter 1> ) )) +
- ((<parameter 3> ) )
-mystrncat.c:12:3: Possible out-of-bounds store. Unable to resolve constraint:
- requires: : maxRead ((buffer @ mystrncat.c:12:13 ) ) <= ( 0 )
+ requires maxSet(buffer @ mystrncat.c:12:13) >= maxRead(buffer @
+ mystrncat.c:12:13) + 255
+ derived from mystrncat precondition:
+ requires maxSet(<parameter 1>) >= maxRead(<parameter 1>) + <parameter 3>
+mystrncat.c:13:3: Possible out-of-bounds store:
+ mystrncat(b, str, sizeof((buffer)) - 1)
+ Unable to resolve constraint:
+ requires maxRead(malloc(256) @ mystrncat.c:10:7) <= 0
needed to satisfy precondition:
- requires: : maxSet ((buffer @ mystrncat.c:12:13 ) ) >= (maxRead ((buffer
- @ mystrncat.c:12:13 ) )) + (( 255 ) )
- derived from mystrncat precondition: requires: :
- maxSet ((<parameter 1> ) ) >= (maxRead ((<parameter 1> ) )) +
- ((<parameter 3> ) )
+ requires maxSet(b @ mystrncat.c:13:13) >= maxRead(b @ mystrncat.c:13:13) +
+ 255
+ derived from mystrncat precondition:
+ requires maxSet(<parameter 1>) >= maxRead(<parameter 1>) + <parameter 3>
-Finished LCLint checking --- 4 code errors found, as expected
+Finished checking --- 4 code warnings, as expected