diff options
| -rw-r--r-- | cparser/Checks.ml | 94 | ||||
| -rw-r--r-- | cparser/Checks.mli | 16 | ||||
| -rw-r--r-- | cparser/Parse.ml | 6 |
3 files changed, 114 insertions, 2 deletions
diff --git a/cparser/Checks.ml b/cparser/Checks.ml new file mode 100644 index 00000000..c64e1a12 --- /dev/null +++ b/cparser/Checks.ml @@ -0,0 +1,94 @@ +(* *********************************************************************) +(* *) +(* 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 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 (sto,id,ty,init) -> unknown_attrs_typ env s.sloc ty + +let unknown_attrs_program p = + let rec transf_globdecls env = function + | [] -> () + | g :: gl -> + let env' = + match g.gdesc with + | Gdecl (sto, id, ty, init) -> + unknown_attrs_typ env g.gloc ty; + Env.add_ident env id sto ty + | Gfundef f -> + unknown_attrs g.gloc f.fd_attrib; + unknown_attrs_stmt env f.fd_body; + 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 diff --git a/cparser/Checks.mli b/cparser/Checks.mli new file mode 100644 index 00000000..34185542 --- /dev/null +++ b/cparser/Checks.mli @@ -0,0 +1,16 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +val program: C.program -> unit diff --git a/cparser/Parse.ml b/cparser/Parse.ml index dceb9b11..0d3003aa 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -23,8 +23,10 @@ let transform_program t p name = (run_pass PackedStructs.program 'p' (run_pass Unblock.program 'b' (run_pass Bitfields.program 'f' - p)))) in - (Rename.program p1) + p)))) in + let p2 = Rename.program p1 in + Checks.program p2; + p2 let parse_transformations s = let t = ref CharSet.empty in |