andersk Git - splint.git/blame_incremental

... / ...

Commit	Line	Data
	1
	2	file1.c: (in function main)
	3	file1.c:10:14: Invalid transfer from implicitly unopen fle to open (unopen file
	4	passed as open): checkOpen(..., fle, ...)
	5	file1.c:6:14: fle becomes implicitly unopen
	6	file1.c:1:53: parameter 1 becomes open
	7	file1.c:19:16: Invalid transfer from implicitly open fle to unopen (open file
	8	passed as unopen): checkClosed(..., fle, ...)
	9	file1.c:12:3: fle becomes implicitly open
	10	file1.c:2:57: parameter 1 becomes unopen
	11	file1.c:23:14: Invalid transfer from unopen fle to open (unopen file passed as
	12	open): checkOpen(..., fle, ...)
	13	file1.c:22:10: fle becomes unopen
	14	file1.c:1:53: parameter 1 becomes open
	15	file1.c:7:8: Variable s declared but not used
	16
	17	Finished checking --- 4 code warnings, as expected
	18
	19	file2.c: (in function main)
	20	file2.c:11:6: Scope exit loses reference fle2 in invalid state implicitly open
	21	(open file not closed)
	22	file2.c:9:41: State becomes implicitly open
	23	file2.c:13:12: Return loses reference fle1 in invalid state implicitly open
	24	(open file not closed)
	25	file2.c:5:37: State becomes implicitly open
	26
	27	Finished checking --- 2 code warnings, as expected
	28
	29	file3.c: (in function main)
	30	file3.c:10:22: Possibly null storage fle1 passed as non-null param:
	31	fclose (fle1)
	32	file3.c:6:16: Storage fle1 may become null
	33	file3.c:11:5: Control branches merge with incompatible states for fle1 (unopen
	34	and open): files merge in inconsistent state
	35	file3.c:6:37: fle1 becomes implicitly open
	36	file3.c:10:14: fle1 becomes unopen
	37
	38	Finished checking --- 2 code warnings, as expected
	39
	40	file4.c: (in function main)
	41	file4.c:15:14: Invalid transfer from implicitly unopen fle to open (unopen file
	42	passed as open): checkOpen(..., fle, ...)
	43	file4.c:11:14: fle becomes implicitly unopen
	44	file4.c:1:53: parameter 1 becomes open
	45
	46	Finished checking --- 1 code warning, as expected
	47
	48	file5.c: (in function passOpen)
	49	file5.c:8:2: Ensures clause not satisfied by f (state is open):
	50	ensures closed f
	51	file5.c:4:35: f becomes open
	52	file5.c: (in function returnOpen)
	53	file5.c:16:10: Result state fle does not satisfy ensures clause:
	54	ensures open result (state is unopen, should be open): fle
	55	file5.c:13:30: Storage fle becomes dependent
	56	file5.c: (in function main)
	57	file5.c:25:14: Invalid transfer from implicitly unopen fle to open (unopen file
	58	passed as open): checkOpen(..., fle, ...)
	59	file5.c:21:14: fle becomes implicitly unopen
	60	file5.c:1:53: parameter 1 becomes open
	61	file5.c:35:18: Invalid transfer from unopen fle to open (unopen file passed as
	62	open): fclose(..., fle, ...)
	63	file5.c:34:3: fle becomes unopen
	64	file.xh:1:44: parameter 1 becomes open
	65
	66	Finished checking --- 4 code warnings, as expected
	67
	68	file6.c: (in function newOpenBad)
	69	file6.c:20:10: Invalid transfer from unopen res to open (unopen file passed as
	70	open): return res
	71	file6.c:19:10: res becomes unopen
	72	file6.c:14:2: becomes open
	73	file6.c: (in function main)
	74	file6.c:30:12: Return loses reference fle in invalid state implicitly open
	75	(open file not closed)
	76	file6.c:27:3: State becomes implicitly open
	77
	78	Finished checking --- 2 code warnings, as expected
	79
	80	filebad.c:1:23: Attribute annotation open used in inconsistent context:
	81	int badOpen(FILE *)
	82	filebad.c:3:52: Attribute annotation closed used in inconsistent context:
	83	int p_x
	84	filebad.c:3:12: Attribute annotation open used on inappropriate reference p_x
	85	in ensures open clause of badEnsures: ensures open p_x
	86
	87	Finished checking --- 3 code warnings, as expected
	88
	89	sockets.c: (in function test1)
	90	sockets.c:13:3: Requires clause of called function useSockets not satisfied
	91	(state is uninitialized): requires sockets_initialized
	92	sockets.c: (in function test5)
	93	sockets.c:37:3: Requires clause of called function useSockets not satisfied
	94	(state is uninitialized): requires sockets_initialized
	95	sockets.c: (in function test6)
	96	sockets.c:42:3: Requires clause of called function useSockets not satisfied
	97	(state is uninitialized): requires sockets_initialized
	98
	99	Finished checking --- 3 code warnings, as expected
	100
	101	sockets2.c: (in function test1)
	102	sockets2.c:15:4: Control branches merge with incompatible global states
	103	(initialized and uninitialized): Sockets initialized on true branch,
	104	uninitialized on false branch.
	105	sockets2.c:11:24: <global marker> becomes uninitialized
	106	sockets2.c:14:5: <global marker> becomes initialized
	107	sockets2.c: (in function test2)
	108	sockets2.c:24:3: Control branches merge with incompatible global states
	109	(uninitialized and initialized): Sockets uninitialized on false branch,
	110	initialized on true branch.
	111	sockets2.c:20:24: <global marker> becomes initialized
	112	sockets2.c:23:5: <global marker> becomes uninitialized
	113
	114	Finished checking --- 2 code warnings, as expected
	115
	116	struct.c: (in function source_badClose)
	117	struct.c:10:2: Function returns with parameter s in inconsistent state (s->file
	118	is unopen, should be open): unopen file passed as open
	119	struct.c:9:10: s->file becomes unopen
	120
	121	Finished checking --- 1 code warning, as expected
	122
	123	nullbranch.c: (in function ftest2)
	124	nullbranch.c:30:22: Possibly null storage f passed as non-null param:
	125	fclose (f)
	126	nullbranch.c:22:7: Storage f may become null
	127	nullbranch.c:32:2: Return loses reference f in invalid state open (open file
	128	not closed)
	129	nullbranch.c:22:3: State becomes open
	130
	131	Finished checking --- 2 code warnings, as expected
	132
	133	osd.c: (in function osd_fileIsReadable)
	134	osd.c:9:7: Return value (type int) ignored: fclose(fl)
	135	osd.c:10:14: Return value type bool does not match declared type int: (TRUE)
	136
	137	Finished checking --- 2 code warnings, as expected