diff options
| -rw-r--r-- | cparser/Cutil.ml | 22 | ||||
| -rw-r--r-- | cparser/Cutil.mli | 2 | ||||
| -rw-r--r-- | cparser/Elab.ml | 2 |
3 files changed, 24 insertions, 2 deletions
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index ea9713d5..b926e84a 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -163,7 +163,10 @@ let rec unroll env t = unroll env (add_attributes_type attr ty) | _ -> t -(* Extracting the attributes of a type *) +(* Extracting the attributes of a type, including the attributes + attached to typedefs, structs and unions. In other words, + typedefs are unrolled and composite definitions expanded + before extracting the attributes. *) let rec attributes_of_type env t = match t with @@ -190,6 +193,23 @@ let rec attributes_of_type env t = | exception Env.Error(Env.Unbound_tag _) -> a end +(* Extracting the attributes of a type, excluding the attributes + attached to typedefs, structs and unions. In other words, + typedefs are not unrolled and composite definitions are not expanded. *) + +let rec attributes_of_type_no_expand t = + match t with + | TVoid a -> a + | TInt(ik, a) -> a + | TFloat(fk, a) -> a + | TPtr(ty, a) -> a + | TArray(ty, sz, a) -> add_attributes a (attributes_of_type_no_expand ty) + | TFun(ty, params, vararg, a) -> a + | TNamed(s, a) -> a + | TStruct(s, a) -> a + | TUnion(s, a) -> a + | TEnum(s, a) -> a + (* Changing the attributes of a type (at top-level) *) (* Same hack as above for array types. *) diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index dc9dc0cc..a99bf3af 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -50,6 +50,8 @@ val remove_custom_attributes : string list -> attributes -> attributes in the given list of names. *) val attributes_of_type : Env.t -> typ -> attributes (* Return the attributes of the given type, expanding typedefs if needed. *) +val attributes_of_type_no_expand : typ -> attributes + (* Return the attributes of the given type, without expanding typedefs. *) val add_attributes_type : attributes -> typ -> typ (* Add the given set of attributes to those of the given type. *) val remove_attributes_type : Env.t -> attributes -> typ -> typ diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 8f27b2a0..8f42fe0a 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -598,7 +598,7 @@ let get_nontype_attrs env ty = | Attr_type -> false | Attr_function -> not (is_function_type env ty) | _ -> true in - let nta = List.filter to_be_removed (attributes_of_type env ty) in + let nta = List.filter to_be_removed (attributes_of_type_no_expand ty) in (remove_attributes_type env nta ty, nta) (* Elaboration of a type specifier. Returns 6-tuple: |