[splint.git] / test / buffertest.expect


buffertest1.c: (in function t1)
buffertest1.c:5:3: Variable g used before definition
buffertest1.c:5:3: Possible out-of-bounds store:
    Unable to resolve constraint:
    requires maxSet(g @ buffertest1.c:5:3) >= 100
     needed to satisfy precondition:
    requires maxSet(g @ buffertest1.c:5:3) >= 100
buffertest1.c: (in function t2)
buffertest1.c:20:3: Variable g used before definition
buffertest1.c:21:3: Possible out-of-bounds store:
    Unable to resolve constraint:
    requires maxSet(g @ buffertest1.c:20:3) >= 1
     needed to satisfy precondition:
    requires maxSet(g @ buffertest1.c:21:3) >= 0
buffertest1.c:21:10: Possible out-of-bounds read:
    Unable to resolve constraint:
    requires maxRead(g @ buffertest1.c:20:3) >= 2
     needed to satisfy precondition:
    requires maxRead(g @ buffertest1.c:21:10) >= 1

Finished checking --- 5 code warnings, as expected
Commit	Line	Data
a469ccf0	1
	2	buffertest1.c: (in function t1)
	3	buffertest1.c:5:3: Variable g used before definition
	4	buffertest1.c:5:3: Possible out-of-bounds store:
	5	Unable to resolve constraint:
	6	requires maxSet(g @ buffertest1.c:5:3) >= 100
	7	needed to satisfy precondition:
	8	requires maxSet(g @ buffertest1.c:5:3) >= 100
	9	buffertest1.c: (in function t2)
	10	buffertest1.c:20:3: Variable g used before definition
	11	buffertest1.c:21:3: Possible out-of-bounds store:
	12	Unable to resolve constraint:
	13	requires maxSet(g @ buffertest1.c:20:3) >= 1
	14	needed to satisfy precondition:
	15	requires maxSet(g @ buffertest1.c:21:3) >= 0
	16	buffertest1.c:21:10: Possible out-of-bounds read:
	17	Unable to resolve constraint:
	18	requires maxRead(g @ buffertest1.c:20:3) >= 2
	19	needed to satisfy precondition:
	20	requires maxRead(g @ buffertest1.c:21:10) >= 1
	21
11db3170	22	Finished checking --- 5 code warnings, as expected