]>
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 | |
0bf5022d | 4 | passed as open): checkOpen(..., fle, ...) |
5 | file1.c:6:14: fle becomes implicitly unopen | |
b7e84605 | 6 | file1.c:1:53: parameter 1 becomes open |
80ee600a | 7 | file1.c:19:16: Invalid transfer from implicitly open fle to unopen (open file |
0bf5022d | 8 | passed as unopen): checkClosed(..., fle, ...) |
9 | file1.c:12:3: fle becomes implicitly open | |
b7e84605 | 10 | file1.c:2:57: parameter 1 becomes unopen |
80ee600a | 11 | file1.c:23:14: Invalid transfer from unopen fle to open (unopen file passed as |
0bf5022d | 12 | open): checkOpen(..., fle, ...) |
13 | file1.c:22:10: fle becomes unopen | |
b7e84605 | 14 | file1.c:1:53: parameter 1 becomes open |
80ee600a | 15 | file1.c:7:8: Variable s declared but not used |
16 | ||
11db3170 | 17 | Finished checking --- 4 code warnings, as expected |
80ee600a | 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 | ||
11db3170 | 27 | Finished checking --- 2 code warnings, as expected |
80ee600a | 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 | |
990ec868 | 34 | and open): files merge in inconsistent state |
0bf5022d | 35 | file3.c:6:37: fle1 becomes implicitly open |
36 | file3.c:10:14: fle1 becomes unopen | |
80ee600a | 37 | |
11db3170 | 38 | Finished checking --- 2 code warnings, as expected |
80ee600a | 39 | |
40 | file4.c: (in function main) | |
41 | file4.c:15:14: Invalid transfer from implicitly unopen fle to open (unopen file | |
0bf5022d | 42 | passed as open): checkOpen(..., fle, ...) |
43 | file4.c:11:14: fle becomes implicitly unopen | |
b7e84605 | 44 | file4.c:1:53: parameter 1 becomes open |
80ee600a | 45 | |
11db3170 | 46 | Finished checking --- 1 code warning, as expected |
80ee600a | 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 | |
0bf5022d | 51 | file5.c:4:35: f becomes open |
80ee600a | 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 | |
80ee600a | 56 | file5.c: (in function main) |
57 | file5.c:25:14: Invalid transfer from implicitly unopen fle to open (unopen file | |
0bf5022d | 58 | passed as open): checkOpen(..., fle, ...) |
59 | file5.c:21:14: fle becomes implicitly unopen | |
b7e84605 | 60 | file5.c:1:53: parameter 1 becomes open |
80ee600a | 61 | file5.c:35:18: Invalid transfer from unopen fle to open (unopen file passed as |
0bf5022d | 62 | open): fclose(..., fle, ...) |
63 | file5.c:34:3: fle becomes unopen | |
53a89507 | 64 | file.xh:1:44: parameter 1 becomes open |
80ee600a | 65 | |
11db3170 | 66 | Finished checking --- 4 code warnings, as expected |
80ee600a | 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 | |
0bf5022d | 71 | file6.c:19:10: res becomes unopen |
b7e84605 | 72 | file6.c:14:2: becomes open |
80ee600a | 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 | ||
11db3170 | 78 | Finished checking --- 2 code warnings, as expected |
80ee600a | 79 | |
0bf5022d | 80 | filebad.c:1:23: Attribute annotation open used in inconsistent context: |
80ee600a | 81 | int badOpen(FILE *) |
0bf5022d | 82 | filebad.c:3:52: Attribute annotation closed used in inconsistent context: |
ccf0a4a8 | 83 | int p_x |
0bf5022d | 84 | filebad.c:3:12: Attribute annotation open used on inappropriate reference p_x |
80ee600a | 85 | in ensures open clause of badEnsures: ensures open p_x |
80ee600a | 86 | |
11db3170 | 87 | Finished checking --- 3 code warnings, as expected |
80ee600a | 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 | ||
11db3170 | 99 | Finished checking --- 3 code warnings, as expected |
80ee600a | 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. | |
0bf5022d | 105 | sockets2.c:11:24: <global marker> becomes uninitialized |
106 | sockets2.c:14:5: <global marker> becomes initialized | |
80ee600a | 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. | |
0bf5022d | 111 | sockets2.c:20:24: <global marker> becomes initialized |
112 | sockets2.c:23:5: <global marker> becomes uninitialized | |
80ee600a | 113 | |
11db3170 | 114 | Finished checking --- 2 code warnings, as expected |
80ee600a | 115 | |
116 | struct.c: (in function source_badClose) | |
b7e84605 | 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 | |
0bf5022d | 119 | struct.c:9:10: s->file becomes unopen |
80ee600a | 120 | |
11db3170 | 121 | Finished checking --- 1 code warning, as expected |
80ee600a | 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) | |
b7e84605 | 129 | nullbranch.c:22:3: State becomes open |
80ee600a | 130 | |
11db3170 | 131 | Finished checking --- 2 code warnings, as expected |
80ee600a | 132 | |
80ee600a | 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 | ||
11db3170 | 137 | Finished checking --- 2 code warnings, as expected |