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