[splint.git] / test / mystrncat.out


mystrncat.c: (in function func)
mystrncat.c:12:13: Passed storage buffer not completely defined (*buffer is
                      undefined): mystrncat (buffer, ...)
mystrncat.c:13:13: Passed storage b not completely defined (*b is undefined):
                      mystrncat (b, ...)
mystrncat.c:12:3: Possible out-of-bounds store:
    Unable to resolve constraint:
    requires maxRead(buffer @ mystrncat.c:12:13) <= 0
     needed to satisfy precondition:
    requires maxSet(buffer @ mystrncat.c:12:13) >= maxRead(buffer @
    mystrncat.c:12:13) + 255
     derived from mystrncat precondition:
    requires maxSet(<parameter 1>) >= maxRead(<parameter 1>) + <parameter 3>
mystrncat.c:13:3: Possible out-of-bounds store:
    Unable to resolve constraint:
    requires maxRead(malloc(256) @ mystrncat.c:10:7) <= 0
     needed to satisfy precondition:
    requires maxSet(b @ mystrncat.c:13:13) >= maxRead(b @ mystrncat.c:13:13) +
    255
     derived from mystrncat precondition:
    requires maxSet(<parameter 1>) >= maxRead(<parameter 1>) + <parameter 3>

Finished checking --- 4 code warnings, as expected
Commit	Line	Data
86d93ed3	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:12:3: Possible out-of-bounds store:
	8	Unable to resolve constraint:
	9	requires maxRead(buffer @ mystrncat.c:12:13) <= 0
	10	needed to satisfy precondition:
	11	requires maxSet(buffer @ mystrncat.c:12:13) >= maxRead(buffer @
	12	mystrncat.c:12:13) + 255
	13	derived from mystrncat precondition:
	14	requires maxSet(<parameter 1>) >= maxRead(<parameter 1>) + <parameter 3>
	15	mystrncat.c:13:3: Possible out-of-bounds store:
	16	Unable to resolve constraint:
	17	requires maxRead(malloc(256) @ mystrncat.c:10:7) <= 0
	18	needed to satisfy precondition:
	19	requires maxSet(b @ mystrncat.c:13:13) >= maxRead(b @ mystrncat.c:13:13) +
	20	255
	21	derived from mystrncat precondition:
	22	requires maxSet(<parameter 1>) >= maxRead(<parameter 1>) + <parameter 3>
	23
	24	Finished checking --- 4 code warnings, as expected