undefined): mystrncat (buffer, ...)
mystrncat.c:13:13: Passed storage b not completely defined (*b is undefined):
mystrncat (b, ...)
-mystrncat.c:12:3: Possible out-of-bounds store. Unable to resolve constraint:
+mystrncat.c:12:3: Possible out-of-bounds store:
+ Unable to resolve constraint:
requires maxRead(buffer @ mystrncat.c:12:13) <= 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>
-mystrncat.c:13:3: Possible out-of-bounds store. Unable to resolve constraint:
+mystrncat.c:13:3: Possible out-of-bounds store:
+ Unable to resolve constraint:
requires maxRead(malloc(256) @ mystrncat.c:10:7) <= 0
needed to satisfy precondition:
requires maxSet(b @ mystrncat.c:13:13) >= maxRead(b @ mystrncat.c:13:13) +