]>
Commit | Line | Data |
---|---|---|
80ee600a | 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): fle | |
5 | file1.c:19:16: Invalid transfer from implicitly open fle to unopen (open file | |
6 | passed as unopen): fle | |
7 | file1.c:12:3: Meta state fle becomes implicitly open | |
8 | file1.c:23:14: Invalid transfer from unopen fle to open (unopen file passed as | |
9 | open): fle | |
10 | file1.c:22:10: Meta state fle becomes unopen | |
11 | file1.c:7:8: Variable s declared but not used | |
12 | ||
13 | Finished LCLint checking --- 4 code errors found, as expected | |
14 | ||
15 | file2.c: (in function main) | |
16 | file2.c:11:6: Scope exit loses reference fle2 in invalid state implicitly open | |
17 | (open file not closed) | |
18 | file2.c:9:41: State becomes implicitly open | |
19 | file2.c:13:12: Return loses reference fle1 in invalid state implicitly open | |
20 | (open file not closed) | |
21 | file2.c:5:37: State becomes implicitly open | |
22 | ||
23 | Finished LCLint checking --- 2 code errors found, as expected | |
24 | ||
25 | file3.c: (in function main) | |
26 | file3.c:10:22: Possibly null storage fle1 passed as non-null param: | |
27 | fclose (fle1) | |
28 | file3.c:6:16: Storage fle1 may become null | |
29 | file3.c:11:5: Control branches merge with incompatible states for fle1 (unopen | |
30 | and implicitly open): files merge in inconsistent state | |
31 | file3.c:6:37: Meta state fle1 becomes implicitly open | |
32 | file3.c:10:14: Meta state fle1 becomes unopen | |
33 | ||
34 | Finished LCLint checking --- 2 code errors found, as expected | |
35 | ||
36 | file4.c: (in function main) | |
37 | file4.c:15:14: Invalid transfer from implicitly unopen fle to open (unopen file | |
38 | passed as open): fle | |
39 | ||
40 | Finished LCLint checking --- 1 code error found, as expected | |
41 | ||
42 | file5.c: (in function passOpen) | |
43 | file5.c:8:2: Ensures clause not satisfied by f (state is open): | |
44 | ensures closed f | |
45 | file5.c:4:35: Meta state f becomes open | |
46 | file5.c: (in function returnOpen) | |
47 | file5.c:16:10: Result state fle does not satisfy ensures clause: | |
48 | ensures open result (state is unopen, should be open): fle | |
49 | file5.c:13:30: Storage fle becomes dependent | |
50 | file5.c:16:10: Dependent storage fle returned as implicitly temp: 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): fle | |
55 | file5.c:35:18: Invalid transfer from unopen fle to open (unopen file passed as | |
56 | open): fle | |
57 | file5.c:34:3: Meta state fle becomes unopen | |
58 | ||
59 | Finished LCLint checking --- 5 code errors found, as expected | |
60 | ||
61 | file6.c: (in function newOpenBad) | |
62 | file6.c:20:10: Invalid transfer from unopen res to open (unopen file passed as | |
63 | open): return res | |
64 | file6.c:19:10: Meta state res becomes unopen | |
65 | file6.c: (in function main) | |
66 | file6.c:30:12: Return loses reference fle in invalid state implicitly open | |
67 | (open file not closed) | |
68 | file6.c:27:3: State becomes implicitly open | |
69 | ||
70 | Finished LCLint checking --- 2 code errors found, as expected | |
71 | ||
72 | filebad.c:1:23: Meta state anntation open used in inconsistent context: | |
73 | int badOpen(FILE *) | |
74 | filebad.c:3:12: Meta state anntation open used on inappropriate reference p_x | |
75 | in ensures open clause of badEnsures: ensures open p_x | |
76 | filebad.c:3:12: Meta state anntation closed used on inappropriate reference p_x | |
77 | in requires closed clause of badEnsures: requires closed p_x | |
78 | ||
79 | Finished LCLint checking --- 3 code errors found, as expected | |
80 | ||
81 | sockets.c: (in function test1) | |
82 | sockets.c:13:3: Requires clause of called function useSockets not satisfied | |
83 | (state is uninitialized): requires sockets_initialized | |
84 | sockets.c: (in function test5) | |
85 | sockets.c:37:3: Requires clause of called function useSockets not satisfied | |
86 | (state is uninitialized): requires sockets_initialized | |
87 | sockets.c: (in function test6) | |
88 | sockets.c:42:3: Requires clause of called function useSockets not satisfied | |
89 | (state is uninitialized): requires sockets_initialized | |
90 | ||
91 | Finished LCLint checking --- 3 code errors found, as expected | |
92 | ||
93 | sockets2.c: (in function test1) | |
94 | sockets2.c:15:4: Control branches merge with incompatible global states | |
95 | (initialized and uninitialized): Sockets initialized on true branch, | |
96 | uninitialized on false branch. | |
97 | sockets2.c:11:24: Meta state <global marker> becomes uninitialized | |
98 | sockets2.c:14:5: Meta state <global marker> becomes initialized | |
99 | sockets2.c: (in function test2) | |
100 | sockets2.c:24:3: Control branches merge with incompatible global states | |
101 | (uninitialized and initialized): Sockets uninitialized on false branch, | |
102 | initialized on true branch. | |
103 | sockets2.c:20:24: Meta state <global marker> becomes initialized | |
104 | sockets2.c:23:5: Meta state <global marker> becomes uninitialized | |
105 | ||
106 | Finished LCLint checking --- 2 code errors found, as expected | |
107 | ||
108 | struct.c: (in function source_badClose) | |
109 | struct.c:25:2: Invalid transfer from unopen s->file to open | |
110 | struct.c:24:10: Meta state s->file becomes unopen | |
111 | ||
112 | Finished LCLint checking --- 1 code error found, as expected | |
113 | ||
114 | nullbranch.c: (in function ftest2) | |
115 | nullbranch.c:30:22: Possibly null storage f passed as non-null param: | |
116 | fclose (f) | |
117 | nullbranch.c:22:7: Storage f may become null | |
118 | nullbranch.c:32:2: Return loses reference f in invalid state open (open file | |
119 | not closed) | |
120 | nullbranch.c:31:5: State becomes open | |
121 | ||
122 | Finished LCLint checking --- 2 code errors found, as expected | |
123 | ||
124 | tainted.c: (in function f) | |
125 | tainted.c:3:20: Invalid transfer from tainted s to untainted (Possibly tainted | |
126 | storage used as untainted.): s | |
127 | tainted.c:1:48: Meta state s becomes tainted | |
128 | tainted.c: (in function test) | |
129 | tainted.c:9:18: Invalid transfer from tainted s to untainted (Possibly tainted | |
130 | storage used as untainted.): s | |
131 | tainted.c:7:34: Meta state s becomes tainted | |
132 | ||
133 | Finished LCLint checking --- 2 code errors found, as expected | |
134 | ||
135 | tainted-bad.mts:18:7: Transfer clause uses unrecognized result state peach: | |
136 | untainted as tainted ==> peach | |
137 | tainted-bad.mts:14:17: Merge clause uses unrecognized second value junky: | |
138 | tainted X junky ==> error "Splat!" | |
139 | tainted-bad.mts:11:7: Annotation declaration uses unrecognized value name blue: | |
140 | maybetainted reference ==> blue | |
141 | tainted-bad.mts:5:21: Defaults declaration uses unrecognized value name | |
142 | stainted: stainted reference | |
143 | tainted-bad.mts:7:21: Duplicate defaults declaration for context param: | |
144 | untainted param | |
145 | tainted.c: (in function f) | |
146 | tainted.c:3:20: Invalid transfer from tainted s to untainted (Possibly tainted | |
147 | storage used as untainted.): s | |
148 | tainted.c:1:48: Meta state s becomes tainted | |
149 | tainted.c: (in function test) | |
150 | tainted.c:9:18: Invalid transfer from tainted s to untainted (Possibly tainted | |
151 | storage used as untainted.): s | |
152 | tainted.c:7:34: Meta state s becomes tainted | |
153 | ||
154 | Finished LCLint checking --- 7 code errors found, as expected | |
155 | ||
156 | tainted2.c: (in function test) | |
157 | tainted2.c:20:10: Invalid transfer from tainted stk to implicitly untainted | |
158 | (Possibly tainted storage used as untainted.): return stk | |
159 | tainted2.c:17:14: Meta state stk becomes tainted | |
160 | ||
161 | Finished LCLint checking --- 1 code error found, as expected | |
162 | ||
163 | tainted3.c: (in function test) | |
164 | tainted3.c:7:3: Requires clause of called function checkUntainted not satisfied | |
165 | by def (state is tainted): requires untainted def | |
166 | ||
167 | Finished LCLint checking --- 1 code error found, as expected | |
168 | ||
169 | tainted4.c: (in function test) | |
170 | tainted4.c:6:17: Invalid transfer from tainted def to implicitly untainted | |
171 | tainted4.c:4:36: Meta state def becomes tainted | |
172 | tainted4.c:7:19: Invalid transfer from tainted def to implicitly untainted | |
173 | tainted4.c:4:36: Meta state def becomes tainted | |
174 | tainted4.c:7:3: Requires clause of called function checkUntainted not satisfied | |
175 | by def (state is tainted): requires untainted *def | |
176 | ||
177 | Finished LCLint checking --- 3 code errors found, expected 1 | |
178 | ||
179 | osd.c: (in function osd_fileIsReadable) | |
180 | osd.c:9:7: Return value (type int) ignored: fclose(fl) | |
181 | osd.c:10:14: Return value type bool does not match declared type int: (TRUE) | |
182 | ||
183 | Finished LCLint checking --- 2 code errors found, as expected |