]>
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 | |
6970c11b | 5 | file1.c:6:14: Meta state fle becomes implicitly unopen |
80ee600a | 6 | file1.c:19:16: Invalid transfer from implicitly open fle to unopen (open file |
7 | passed as unopen): fle | |
8 | file1.c:12:3: Meta state fle becomes implicitly open | |
9 | file1.c:23:14: Invalid transfer from unopen fle to open (unopen file passed as | |
10 | open): fle | |
11 | file1.c:22:10: Meta state fle becomes unopen | |
12 | file1.c:7:8: Variable s declared but not used | |
13 | ||
14 | Finished LCLint checking --- 4 code errors found, as expected | |
15 | ||
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 | |
23 | ||
24 | Finished LCLint checking --- 2 code errors found, as expected | |
25 | ||
26 | file3.c: (in function main) | |
27 | file3.c:10:22: Possibly null storage fle1 passed as non-null param: | |
28 | fclose (fle1) | |
29 | file3.c:6:16: Storage fle1 may become null | |
30 | file3.c:11:5: Control branches merge with incompatible states for fle1 (unopen | |
990ec868 | 31 | and open): files merge in inconsistent state |
80ee600a | 32 | file3.c:6:37: Meta state fle1 becomes implicitly open |
33 | file3.c:10:14: Meta state fle1 becomes unopen | |
34 | ||
35 | Finished LCLint checking --- 2 code errors found, as expected | |
36 | ||
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): fle | |
6970c11b | 40 | file4.c:11:14: Meta state fle becomes implicitly unopen |
80ee600a | 41 | |
42 | Finished LCLint checking --- 1 code error found, as expected | |
43 | ||
44 | file5.c: (in function passOpen) | |
45 | file5.c:8:2: Ensures clause not satisfied by f (state is open): | |
46 | ensures closed f | |
47 | file5.c:4:35: Meta state 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 | |
80ee600a | 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 | |
6970c11b | 55 | file5.c:21:14: Meta state fle becomes implicitly unopen |
80ee600a | 56 | file5.c:35:18: Invalid transfer from unopen fle to open (unopen file passed as |
57 | open): fle | |
58 | file5.c:34:3: Meta state fle becomes unopen | |
59 | ||
ccf0a4a8 | 60 | Finished LCLint checking --- 4 code errors found, as expected |
80ee600a | 61 | |
62 | file6.c: (in function newOpenBad) | |
63 | file6.c:20:10: Invalid transfer from unopen res to open (unopen file passed as | |
64 | open): return res | |
65 | file6.c:19:10: Meta state 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 | |
70 | ||
71 | Finished LCLint checking --- 2 code errors found, as expected | |
72 | ||
6970c11b | 73 | filebad.c:1:23: Meta state annotation open used in inconsistent context: |
80ee600a | 74 | int badOpen(FILE *) |
6970c11b | 75 | filebad.c:3:52: Meta state annotation closed used in inconsistent context: |
ccf0a4a8 | 76 | int p_x |
6970c11b | 77 | filebad.c:3:12: Meta state annotation open used on inappropriate reference p_x |
80ee600a | 78 | in ensures open clause of badEnsures: ensures open p_x |
80ee600a | 79 | |
80 | Finished LCLint checking --- 3 code errors found, as expected | |
81 | ||
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 | |
91 | ||
92 | Finished LCLint checking --- 3 code errors found, as expected | |
93 | ||
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: Meta state <global marker> becomes uninitialized | |
99 | sockets2.c:14:5: Meta state <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: Meta state <global marker> becomes initialized | |
105 | sockets2.c:23:5: Meta state <global marker> becomes uninitialized | |
106 | ||
107 | Finished LCLint checking --- 2 code errors found, as expected | |
108 | ||
109 | struct.c: (in function source_badClose) | |
b072092f | 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: Meta state s->file becomes unopen | |
80ee600a | 113 | |
114 | Finished LCLint checking --- 1 code error found, as expected | |
115 | ||
116 | nullbranch.c: (in function ftest2) | |
117 | nullbranch.c:30:22: Possibly null storage f passed as non-null param: | |
118 | fclose (f) | |
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 | |
121 | not closed) | |
122 | nullbranch.c:31:5: State becomes open | |
123 | ||
124 | Finished LCLint checking --- 2 code errors found, as expected | |
125 | ||
80ee600a | 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) | |
129 | ||
130 | Finished LCLint checking --- 2 code errors found, as expected |