andersk Git - splint.git/blame_incremental

... / ...

Commit	Line	Data
	1
	2	mystrncat.c: (in function func)
	3	mystrncat.c:12:13: Passed storage buffer not completely defined (*buffer is
	4	undefined): mystrncat (buffer, ...)
	5	mystrncat.c:13:13: Passed storage b not completely defined (*b is undefined):
	6	mystrncat (b, ...)
	7	mystrncat.c:10:3: Storage *b allocated
	8	mystrncat.c:12:3: Possible out-of-bounds store:
	9	mystrncat(buffer, str, sizeof((buffer)) - 1)
	10	Unable to resolve constraint:
	11	requires maxRead(buffer @ mystrncat.c:12:13) <= 0
	12	needed to satisfy precondition:
	13	requires maxSet(buffer @ mystrncat.c:12:13) >= maxRead(buffer @
	14	mystrncat.c:12:13) + 255
	15	derived from mystrncat precondition:
	16	requires maxSet(<parameter 1>) >= maxRead(<parameter 1>) + <parameter 3>
	17	mystrncat.c:13:3: Possible out-of-bounds store:
	18	mystrncat(b, str, sizeof((buffer)) - 1)
	19	Unable to resolve constraint:
	20	requires maxRead(malloc(256) @ mystrncat.c:10:7) <= 0
	21	needed to satisfy precondition:
	22	requires maxSet(b @ mystrncat.c:13:13) >= maxRead(b @ mystrncat.c:13:13) +
	23	255
	24	derived from mystrncat precondition:
	25	requires maxSet(<parameter 1>) >= maxRead(<parameter 1>) + <parameter 3>
	26
	27	Finished checking --- 4 code warnings, as expected