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
|
(* *********************************************************************)
(* *)
(* 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 Cutil
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
Cerrors.warning loc Cerrors.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 unknown_attrs_program p =
let rec transf_globdecls env = function
| [] -> ()
| g :: gl ->
let env' =
match g.gdesc with
| Gdecl ((sto, id, ty, init) as d) ->
unknown_attrs_decl env g.gloc d;
Env.add_ident env id sto ty
| Gfundef f ->
unknown_attrs g.gloc f.fd_attrib;
unknown_attrs_stmt env f.fd_body;
List.iter (unknown_attrs_decl env g.gloc) f.fd_locals;
Env.add_ident env f.fd_name f.fd_storage (fundef_typ f)
| Gcompositedecl(su, id, attr) ->
Env.add_composite env id (composite_info_decl su attr)
| Gcompositedef(su, id, attr, fl) ->
unknown_attrs g.gloc attr;
List.iter (fun fld -> unknown_attrs_typ env g.gloc fld.fld_typ) fl;
Env.add_composite env id (composite_info_def env su attr fl)
| Gtypedef(id, ty) ->
unknown_attrs_typ env g.gloc ty;
Env.add_typedef env id ty
| Genumdef(id, attr, members) ->
unknown_attrs g.gloc attr;
Env.add_enum env id {Env.ei_members = members; ei_attr = attr}
| Gpragma s ->
env
in
transf_globdecls env' gl
in transf_globdecls (Builtins.environment()) p
let program p =
unknown_attrs_program p
|
