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