10 December 2001
David Larochelle
10
strncat.c:4:21: Possible out-of-bounds store:
strncat(buffer, str, sizeof((buffer)) - 1);
Unable to
resolve constraint:
requires
maxRead (buffer @ strncat.c:4:29) <=
0
needed to
satisfy precondition:
requires
maxSet (buffer @ strncat.c:4:29)
>= maxRead (buffer @ strncat.c:4:29) + 255
derived
from strncat precondition:
requires
maxSet (<parameter 1>)
>= maxRead
(<parameter1>) + <parameter 3>
Warning Reported
char
* strncat (char *s1, char *s2, size_t
n)
/*@requires
maxSet(s1) >= maxRead(s1) + n @*/
char buffer[256];
strncat(buffer, str, sizeof(buffer) - 1);