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
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
|
sample.c:11: Fresh storage x not released before
return
sample.c:5: Fresh storage x created
sample.c:5: Variable x declared but not used
Finished checking --- 2 code warnings, as expected
null.c:3: Dereference of possibly null pointer s: *s
null.c:1: Storage s may become null
Finished checking --- 1 code warning, as expected
Finished checking --- no warnings
usedef.c:11: Value *x used before definition
usedef.c:13: Passed storage x not completely defined
(*x is undefined): getVal (x)
usedef.c:15: Passed storage x not completely defined
(*x is undefined): mysteryVal (x)
Finished checking --- 3 code warnings, as expected
usedef.c:11: Value *x used before definition
usedef.c:13: Passed storage x not completely defined
(*x is undefined): getVal (x)
Finished checking --- 2 code warnings, as expected
bool.c:6: Test expression for if is assignment expression: i = 3
bool.c:6: Test expression for if not bool, type int: i = 3
bool.c:7: Return value type bool does not match declared type int: b1
bool.c:8: Operand of ! is non-boolean (int): !i
bool.c:8: Right operand of || is non-boolean (char *): !i || s
bool.c:10: Test expression for if not bool, type char *: s
bool.c:12: Use of == with bool variables (risks inconsistency because
of multiple true values): b1 == b2
Finished checking --- 7 code warnings, as expected
palindrome.c:6: Cast from underlying
abstract type mstring: (char *)s
palindrome.c:7: Function strlen expects arg
1 to be char * gets mstring: s
palindrome.c:11: Array fetch from non-array
(mstring): s[len - i - 1]
palindrome.c:19: Function isPalindrome
expects arg 1 to be mstring gets char *:
"bob"
Finished checking --- 4 code warnings, as
expected
only.c:11: Only storage glob (type int *) not released
before assignment: glob = y
only.c:1: Storage glob becomes only
only.c:11: Implicitly temp storage y assigned to only:
glob = y
only.c:13: Dereference of possibly null pointer m: *m
only.c:8: Storage m may become null
only.c:13: Variable x used after being released
only.c:12: Storage x released
only.c:14: Implicitly temp storage z returned as only:
z
only.c:14: Fresh storage m not released before return
only.c:9: Fresh storage m created
Finished checking --- 6 code warnings, as expected
stack.c:12: Stack-allocated storage &loc reachable
from return value: &loc
stack.c:12: Stack-allocated storage *x reachable from
parameter x
stack.c:10: Storage *x becomes stack-allocated
storage
stack.c:12: Stack-allocated storage glob reachable
from global glob
stack.c:9: Storage glob becomes stack-allocated
storage
Finished checking --- 3 code warnings, as expected
rstring.c:13: Reference counted storage returned
without modifying reference count: r1
Finished checking --- 1 code warning, as expected
unique.c:7: Parameter 1 (s) to function strcpy is
declared unique but may be aliased externally by
parameter 2 (t)
Finished checking --- 1 code warning, as expected
exposure.c:6: Function returns reference to
parameter e: e->name
exposure.c:6: Return value exposes rep of
employee: e->name
exposure.c:6: Released storage e->name reachable
from parameter at return point
exposure.c:6: Storage e->name released
exposure.c:23: Suspect modification of observer
name: *name = toupper(*name)
exposure.c:22: Storage *name becomes observer
Finished checking --- 4 code warnings, as
expected
modify.c:4: Undocumented modification of *y: *y = *x
modify.c:5: Suspect object listed in modifies of setx
not modified: *x
modify.c:1: Declaration of setx
Finished checking --- 2 code warnings, as expected
globals.c:5: Undocumented use of global glob2
globals.c:3: Global glob1 listed but not used
Finished checking --- 2 code warnings, as expected
annotglobs.c:13: Undef global globnum used before
definition
annotglobs.c:15: Global storage globname contains 1
undefined field when call returns: firstname
annotglobs.c:21: Only storage globname.firstname (type
char *) derived from killed global is not released
(memory leak)
Finished checking --- 3 code warnings, as expected
Finished checking --- no warnings
order.c:11: Expression has undefined behavior (value of
right operand modified by left operand): x++ * x
order.c:13: Expression has undefined behavior (left operand
uses i, modified by right operand): y[i] = i++
order.c:14: Expression has undefined behavior (value of
right operand modified by left operand):
modglob() * glob
order.c:15: Expression has undefined behavior
(unconstrained function mystery used in left operand
may set global variable glob used in right operand):
mystery() * glob
Finished checking --- 4 code warnings, as expected
order.c:11: Expression has undefined behavior (value
of right operand modified by left operand):
x++ * x
order.c:13: Expression has undefined behavior (left
operand uses i, modified by right operand):
y[i] = i++
order.c:14: Expression has undefined behavior (value
of right operand modified by left operand):
modglob() * glob
Finished checking --- 3 code warnings, as expected
loop.c:14: Suspected infinite loop. No value used in
loop test (x, glob1) is modified by test or loop
body.
loop.c:15: Suspected infinite loop. No condition
values modified. Modification possible through
unconstrained calls: h
Finished checking --- 2 code warnings, as expected
loop.c:14: Suspected infinite loop. No value used in
loop test (x, glob1) is modified by test or loop
body.
Finished checking --- 1 code warning, as expected
switch.c:11: Fall through case (no preceding break)
switch.c:14: Missing case in switch: DEFINITELY
Finished checking --- 2 code warnings, as expected
noeffect.c:6: Statement has no effect: y == *x
noeffect.c:7: Statement has no effect: nomodcall(x)
noeffect.c:8: Statement has no effect (possible
undected modification through call to
unconstrained function mysterycall):
mysterycall(x)
Finished checking --- 3 code warnings, as expected
noeffect.c:6: Statement has no effect: y == *x
noeffect.c:7: Statement has no effect: nomodcall(x)
Finished checking --- 2 code warnings, as expected
ignore.c:8: Return value (type int) ignored: fi()
ignore.c:10: Return value (type bool) ignored: fb()
Finished checking --- 2 code warnings, as expected
ignore.c:8: Return value (type int) ignored: fi()
Finished checking --- 1 code warning, as expected
ignore.c:10: Return value (type bool) ignored: fb()
Finished checking --- 1 code warning, as expected
setChar.c:5: Likely out-of-bounds store: buf[10]
Unable to resolve constraint:
requires 9 >= 10
needed to satisfy precondition:
requires maxSet(buf @ setChar.c:5) >= 10
Finished checking --- 1 code warning, as expected
multiError.c:4: Possible out-of-bounds store: buf[2]
Unable to resolve constraint:
requires maxSet(buf @ multiError.c:4) >= 2
needed to satisfy precondition:
requires maxSet(buf @ multiError.c:4) >= 2
Finished checking --- 1 code warning, as expected
bounds.c:9: Possible out-of-bounds store:
strcpy(str, tmp)
Unable to resolve constraint:
requires maxSet(str @ bounds.c:9) >=
maxRead(getenv("MYENV") @ bounds.c:7)
needed to satisfy precondition:
requires maxSet(str @ bounds.c:9) >=
maxRead(tmp @ bounds.c:9)
derived from strcpy precondition: requires
maxSet(<parameter 1>) >= maxRead(<parameter
2>)
Finished checking --- 1 code warning, as expected
|
