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
234
235
236
237
238
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU General Public License as published by *)
(* the Free Software Foundation, either version 2 of the License, or *)
(* (at your option) any later version. This file is also distributed *)
(* under the terms of the INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
open C
open Diagnostics
open Cutil
open Env
let attribute_string = function
| AConst -> "const"
| AVolatile -> "volatile"
| ARestrict -> "restrict"
| AAlignas n -> "_Alignas"
| Attr(name, _) -> name
let unknown_attrs loc attrs =
let unknown attr =
let attr_class = class_of_attribute attr in
if attr_class = Attr_unknown then
warning loc Unknown_attribute
"unknown attribute '%s' ignored" (attribute_string attr) in
List.iter unknown attrs
let unknown_attrs_typ env loc ty =
let attr = attributes_of_type env ty in
unknown_attrs loc attr
let unknown_attrs_decl env loc (sto, id, ty, init) =
unknown_attrs_typ env loc ty
let rec unknown_attrs_stmt env s =
match s.sdesc with
| Sskip
| Sbreak
| Scontinue
| Slabeled _
| Sgoto _
| Sreturn _
| Sasm _
| Sdo _ -> ()
| Sif (_,s1,s2)
| Sseq (s1,s2) ->
unknown_attrs_stmt env s1;
unknown_attrs_stmt env s2
| Sfor (s1,e,s2,s3) ->
unknown_attrs_stmt env s1;
unknown_attrs_stmt env s2;
unknown_attrs_stmt env s3
| Swhile(_,s)
| Sdowhile (s,_)
| Sswitch (_,s) -> unknown_attrs_stmt env s
| Sblock sl -> List.iter (unknown_attrs_stmt env) sl
| Sdecl d -> unknown_attrs_decl env s.sloc d
let traverse_program
?(decl = fun env loc d -> ())
?(fundef = fun env loc fd -> ())
?(compositedecl = fun env loc su id attr -> ())
?(compositedef = fun env loc su id attr fl -> ())
?(typedef = fun env loc id ty -> ())
?(enum = fun env loc id attr members -> ())
?(pragma = fun env loc s -> ())
p =
let rec traverse env = function
| [] -> ()
| g :: gl ->
let env =
match g.gdesc with
| Gdecl ((sto, id, ty, init) as d) ->
decl env g.gloc d;
add_ident env id sto ty
| Gfundef f ->
fundef env g.gloc f;
add_ident env f.fd_name f.fd_storage (fundef_typ f)
| Gcompositedecl (su,id,attr) ->
compositedecl env g.gloc su id attr;
add_composite env id (composite_info_decl su attr)
| Gcompositedef (su,id,attr,fl) ->
compositedef env g.gloc su id attr fl;
add_composite env id (composite_info_def env su attr fl)
| Gtypedef (id,ty) ->
typedef env g.gloc id ty;
add_typedef env id ty
| Genumdef (id,attr,members) ->
enum env g.gloc id attr members;
add_enum env id {ei_members = members; ei_attr = attr}
| Gpragma s ->
pragma env g.gloc s;
env in
traverse env gl in
traverse (Builtins.environment ()) p
let unknown_attrs_program p =
let decl env loc d =
unknown_attrs_decl env loc d
and fundef env loc f =
List.iter (fun (id,typ) -> unknown_attrs_typ env loc typ) f.fd_params;
unknown_attrs loc f.fd_attrib;
unknown_attrs_stmt env f.fd_body;
List.iter (unknown_attrs_decl env loc) f.fd_locals;
and compositedecl env loc su id attr =
unknown_attrs loc attr
and compositedef env loc su id attr fl =
unknown_attrs loc attr;
List.iter (fun fld -> unknown_attrs_typ env loc fld.fld_typ) fl
and typedef env loc id ty =
unknown_attrs_typ env loc ty
and enum env loc id attr members =
unknown_attrs loc attr
in
traverse_program
~decl:decl
~fundef:fundef
~compositedecl:compositedecl
~compositedef:compositedef
~typedef:typedef
~enum:enum
p
let rec vars_used_expr env e =
match e.edesc with
| EConst _
| ESizeof _
| EAlignof _ -> env
| EVar id -> IdentSet.add id env
| ECast (_,e)
| EUnop (_,e) -> vars_used_expr env e
| EBinop (_,e1,e2,_) ->
let env = vars_used_expr env e1 in
vars_used_expr env e2
| EConditional (e1,e2,e3) ->
let env = vars_used_expr env e1 in
let env = vars_used_expr env e2 in
vars_used_expr env e3
| ECompound (_,init) -> vars_used_init env init
| ECall (e,p) ->
let env = vars_used_expr env e in
List.fold_left vars_used_expr env p
and vars_used_init env = function
| Init_single e -> vars_used_expr env e
| Init_array al -> List.fold_left vars_used_init env al
| Init_struct (_,sl) -> List.fold_left (fun env (_,i) -> vars_used_init env i) env sl
| Init_union (_,_,ui) -> vars_used_init env ui
let rec vars_used_stmt env s =
match s.sdesc with
| Sbreak
| Scontinue
| Sgoto _
| Sreturn None
| Sskip -> env
| Sreturn (Some e)
| Sdo e -> (vars_used_expr env e)
| Sseq (s1,s2) ->
let env = vars_used_stmt env s1 in
vars_used_stmt env s2
| Sif (e,s1,s2) ->
let env = vars_used_expr env e in
let env = vars_used_stmt env s1 in
vars_used_stmt env s2
| Sfor (s1,e,s2,s3) ->
let env = vars_used_expr env e in
let env = vars_used_stmt env s1 in
let env = vars_used_stmt env s2 in
vars_used_stmt env s3
| Sswitch (e,s)
| Swhile (e,s)
| Sdowhile (s,e) ->
let env = vars_used_expr env e in
vars_used_stmt env s
| Sblock sl -> List.fold_left vars_used_stmt env sl
| Sdecl (sto,id,ty,init) ->
let env = match init with
| Some init ->vars_used_init env init
| None -> env in
env
| Slabeled (lbl,s) -> vars_used_stmt env s
| Sasm (attr,str,op,op2,constr) ->
let vars_asm_op env (_,_,e) =
vars_used_expr env e in
let env = List.fold_left vars_asm_op env op in
let env = List.fold_left vars_asm_op env op2 in
env
let unused_variable env used loc (id,ty) =
let attr = attributes_of_type env ty in
let unused_attr = find_custom_attributes ["unused";"__unused__"] attr <> [] in
if not ((IdentSet.mem id used) || unused_attr) then
warning loc Unused_variable "unused variable '%s'" id.name
let rec unused_variables_stmt env used s =
match s.sdesc with
| Sbreak
| Scontinue
| Sgoto _
| Sreturn _
| Sskip
| Sasm _
| Sdo _ -> ()
| Sseq (s1,s2)
| Sif (_,s1,s2) ->
unused_variables_stmt env used s1;
unused_variables_stmt env used s2
| Sfor (s1,e,s2,s3) ->
unused_variables_stmt env used s1;
unused_variables_stmt env used s2;
unused_variables_stmt env used s3
| Slabeled (_,s)
| Sswitch (_,s)
| Swhile (_,s)
| Sdowhile (s,_) ->
unused_variables_stmt env used s
| Sblock sl -> List.iter (unused_variables_stmt env used) sl
| Sdecl (sto,id,ty,init) ->
unused_variable env used s.sloc (id,ty)
let unused_variables p =
let fundef env loc fd =
let used = vars_used_stmt IdentSet.empty fd.fd_body in
unused_variables_stmt env used fd.fd_body;
List.iter (unused_variable env used loc) fd.fd_params in
traverse_program
~fundef:fundef
p
|
