[splint.git] / test / moreBufferTests.expect


unrecogCall.c: (in function foo)
unrecogCall.c:8:3: Unrecognized identifier: bar
initialization.c: (in function initialization)
initialization.c:5:10: Variable g declared but not used
initialization.c:5:14: Possible out-of-bounds read:
    e[22]
    Unable to resolve constraint:
    requires maxRead(d @ initialization.c:3:14) >= 22
     needed to satisfy precondition:
    requires maxRead(e @ initialization.c:5:14) >= 22
initialization.c:8:3: Possible out-of-bounds store:
    f[2]
    Unable to resolve constraint:
    requires maxSet(d @ initialization.c:3:14) >= 2
     needed to satisfy precondition:
    requires maxSet(f @ initialization.c:8:3) >= 2
simplifyTest.c: (in function fooSub)
simplifyTest.c:3:3: Possible out-of-bounds store:
    s[i]
    Unable to resolve constraint:
    requires maxSet(s @ simplifyTest.c:3:3) >= i @ simplifyTest.c:3:5
     needed to satisfy precondition:
    requires maxSet(s @ simplifyTest.c:3:3) >= i @ simplifyTest.c:3:5
simplifyTest.c: (in function fooAdd)
simplifyTest.c:10:3: Possible out-of-bounds store:
    s[i + 2]
    Unable to resolve constraint:
    requires maxSet(s @ simplifyTest.c:10:3) >= i @ simplifyTest.c:10:5 + 2
     needed to satisfy precondition:
    requires maxSet(s @ simplifyTest.c:10:3) >= i @ simplifyTest.c:10:5 + 2
strncatNotReallyGood.c: (in function NotGoodfunc)
strncatNotReallyGood.c:4:29: Passed storage buffer not completely defined
                                (*buffer is undefined): strncat (buffer, ...)
strncatNotReallyGood.c:4:21: Possible out-of-bounds store:
    strncat(buffer, str, sizeof((buffer)) - 1)
    Unable to resolve constraint:
    requires maxRead(buffer @ strncatNotReallyGood.c:4:29) <= 0
     needed to satisfy precondition:
    requires maxSet(buffer @ strncatNotReallyGood.c:4:29) >= maxRead(buffer @
    strncatNotReallyGood.c:4:29) + 255
     derived from strncat precondition: requires maxSet(<parameter 1>) >=
    maxRead(<parameter 1>) + <parameter 3>

Finished checking --- 8 code warnings, as expected
Commit	Line	Data
80ee600a	1
	2	unrecogCall.c: (in function foo)
	3	unrecogCall.c:8:3: Unrecognized identifier: bar
dcf136ce	4	initialization.c: (in function initialization)
dcf136ce	5	initialization.c:5:10: Variable g declared but not used
7bf96067	6	initialization.c:5:14: Possible out-of-bounds read:
9276a168	7	e[22]
7bf96067	8	Unable to resolve constraint:
4109ede4	9	requires maxRead(d @ initialization.c:3:14) >= 22
03d670b6	10	needed to satisfy precondition:
4109ede4	11	requires maxRead(e @ initialization.c:5:14) >= 22
7bf96067	12	initialization.c:8:3: Possible out-of-bounds store:
9276a168	13	f[2]
7bf96067	14	Unable to resolve constraint:
bf5819c8	15	requires maxSet(d @ initialization.c:3:14) >= 2
	16	needed to satisfy precondition:
	17	requires maxSet(f @ initialization.c:8:3) >= 2
dcf136ce	18	simplifyTest.c: (in function fooSub)
7bf96067	19	simplifyTest.c:3:3: Possible out-of-bounds store:
9276a168	20	s[i]
7bf96067	21	Unable to resolve constraint:
4109ede4	22	requires maxSet(s @ simplifyTest.c:3:3) >= i @ simplifyTest.c:3:5
03d670b6	23	needed to satisfy precondition:
4109ede4	24	requires maxSet(s @ simplifyTest.c:3:3) >= i @ simplifyTest.c:3:5
dcf136ce	25	simplifyTest.c: (in function fooAdd)
7bf96067	26	simplifyTest.c:10:3: Possible out-of-bounds store:
9276a168	27	s[i + 2]
7bf96067	28	Unable to resolve constraint:
4109ede4	29	requires maxSet(s @ simplifyTest.c:10:3) >= i @ simplifyTest.c:10:5 + 2
03d670b6	30	needed to satisfy precondition:
4109ede4	31	requires maxSet(s @ simplifyTest.c:10:3) >= i @ simplifyTest.c:10:5 + 2
6e5d6478	32	strncatNotReallyGood.c: (in function NotGoodfunc)
	33	strncatNotReallyGood.c:4:29: Passed storage buffer not completely defined
	34	(*buffer is undefined): strncat (buffer, ...)
7bf96067	35	strncatNotReallyGood.c:4:21: Possible out-of-bounds store:
9276a168	36	strncat(buffer, str, sizeof((buffer)) - 1)
7bf96067	37	Unable to resolve constraint:
4109ede4	38	requires maxRead(buffer @ strncatNotReallyGood.c:4:29) <= 0
03d670b6	39	needed to satisfy precondition:
4109ede4	40	requires maxSet(buffer @ strncatNotReallyGood.c:4:29) >= maxRead(buffer @
	41	strncatNotReallyGood.c:4:29) + 255
	42	derived from strncat precondition: requires maxSet(<parameter 1>) >=
	43	maxRead(<parameter 1>) + <parameter 3>
80ee600a	44
11db3170	45	Finished checking --- 8 code warnings, as expected