andersk Git - splint.git/blame_incremental - test/moreBufferTests2.expect

... / ...

Commit	Line	Data
	1
	2	unknownsize.c: (in function uknSize1)
	3	unknownsize.c:9:3: Possible out-of-bounds store: c[9]
	4	Unable to resolve constraint:
	5	requires maxSet(c @ unknownsize.c:9:3) >= 9
	6	needed to satisfy precondition:
	7	requires maxSet(c @ unknownsize.c:9:3) >= 9
	8
	9	Finished checking --- 1 code warning, as expected
	10
	11	fixedArrayType.c: (in function fixedArrayTouch)
	12	fixedArrayType.c:9:3: Possible out-of-bounds store: buffer[sizeof(Array) - 1]
	13	Unable to resolve constraint:
	14	requires sizeof(Array) @ fixedArrayType.c:9:25 <= 10
	15	needed to satisfy precondition:
	16	requires maxSet(buffer @ fixedArrayType.c:9:3) >= sizeof(Array) @
	17	fixedArrayType.c:9:25 - 1
	18
	19	Finished checking --- 1 code warning, as expected
	20
	21	initBlock.c: (in function main)
	22	initBlock.c:8:3: Likely out-of-bounds store: buf[10]
	23	Unable to resolve constraint:
	24	requires 9 >= 10
	25	needed to satisfy precondition:
	26	requires maxSet(buf @ initBlock.c:8:3) >= 10
	27
	28	Finished checking --- 1 code warning, as expected