diff --git a/src/kernel_services/ast_queries/ast_attributes.ml b/src/kernel_services/ast_queries/ast_attributes.ml
new file mode 100644
index 0000000000000000000000000000000000000000..cc05a2957c95587f199924e4b0dc6b3f1f2ec87d
--- /dev/null
+++ b/src/kernel_services/ast_queries/ast_attributes.ml
@@ -0,0 +1,272 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2025 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** This file contains attribute related types/functions/values. *)
+
+open Cil_types
+
+let bitfield_attribute_name = "FRAMA_C_BITFIELD_SIZE"
+
+let anonymous_attribute_name = "fc_anonymous"
+
+let anonymous_attribute = Attr(anonymous_attribute_name, [])
+
+let qualifier_attributes = [ "const"; "restrict"; "volatile"; "ghost" ]
+
+let fc_internal_attributes = ["declspec"; "arraylen"; "fc_stdlib"]
+
+let cast_irrelevant_attributes = ["visibility"]
+
+let spare_attributes_for_c_cast = fc_internal_attributes @ qualifier_attributes
+
+let spare_attributes_for_logic_cast = spare_attributes_for_c_cast
+
+(** Construct sorted lists of attributes ***)
+let attribute_name (Attr(an, _) | AttrAnnot an) =
+ Extlib.strip_underscore an
+
+let has_attribute an al =
+ let an = Extlib.strip_underscore an in
+ List.exists (fun a -> attribute_name a = an) al
+
+(* Attributes are added as they are (e.g. if we add ["__attr"] and then ["attr"]
+ both are added). When checking for the presence of an attribute [x] or trying
+ to remove it, underscores are removed at the beginning and the end of the
+ attribute for both the [x] attribute and the attributes of the list. For
+ example, if have a call:
+
+ dropAttribute "__const" [ Attr("const", []) ; Attr("__const", []) ; Attr("__const__", []) ]
+
+ The result is [].
+*)
+
+let add_attribute (Attr(an, _) | AttrAnnot an as a) al =
+ let rec insert_sorted = function
+ | [] -> [a]
+ | ((Attr(an0, _) | AttrAnnot an0 as a0) :: rest) as l ->
+ if an < an0 then a :: l
+ else if Cil_datatype.Attribute.equal a a0 then l (* Do not add if already in there *)
+ else a0 :: insert_sorted rest (* Make sure we see all attributes with
+ * this name *)
+ in
+ insert_sorted al
+
+(** The second attribute list is sorted *)
+let add_attributes al0 al =
+ if al0 == [] then
+ al
+ else
+ List.fold_left (fun acc a -> add_attribute a acc) al al0
+
+let drop_attribute an al =
+ let an = Extlib.strip_underscore an in
+ List.filter (fun a -> attribute_name a <> an) al
+
+let rec drop_attributes anl al =
+ match al with
+ | [] -> []
+ | a :: q ->
+ let q' = drop_attributes anl q in
+ if List.mem (attribute_name a) anl then
+ q' (* drop this attribute *)
+ else
+ if q' == q then al (* preserve sharing *) else a :: q'
+
+let find_attribute an al =
+ let an = Extlib.strip_underscore an in
+ List.fold_left (fun acc a ->
+ match a with
+ | Attr (_, param) as a0 when attribute_name a0 = an -> param @ acc
+ | _ -> acc
+ ) [] al
+
+let filter_attributes an al =
+ let an = Extlib.strip_underscore an in
+ List.filter (fun a -> attribute_name a = an) al
+
+let filter_qualifier_attributes al =
+ List.filter (fun a -> List.mem (attribute_name a) qualifier_attributes) al
+
+let split_array_attributes al =
+ List.partition (fun a -> List.mem (attribute_name a) qualifier_attributes) al
+
+(**************************************)
+(* Attribute registration and classes *)
+(**************************************)
+
+type attribute_class =
+ (** Attribute of a name. If argument is true and we are on MSVC then
+ the attribute is printed using __declspec as part of the storage
+ specifier *)
+ | AttrName of bool
+
+ (** Attribute of a function type. If argument is true and we are on
+ MSVC then the attribute is printed just before the function name *)
+ | AttrFunType of bool
+
+ (** Attribute of a type *)
+ | AttrType
+
+ (** Attribute of a statement or a block *)
+ | AttrStmt
+
+ (** Attribute that does not correspond to either of the above classes and is
+ ignored by functions {!get_attribute_class} and {!partition_attributes}. *)
+ | AttrIgnored
+
+(* This table contains the mapping of predefined attributes to classes.
+ * Extend this table with more attributes as you need. This table is used to
+ * determine how to associate attributes with names or type during cabs2cil
+ * conversion *)
+let attribute_hash : (string, attribute_class) Hashtbl.t =
+ let table = Hashtbl.create 13 in
+ List.iter (fun a -> Hashtbl.add table a (AttrName false))
+ [ "section"; "constructor"; "destructor"; "unused"; "used"; "weak";
+ "no_instrument_function"; "alias"; "no_check_memory_usage";
+ "exception"; "model"; (* "restrict"; *)
+ "aconst"; "asm" (* Gcc uses this to specify the name to be used in
+ * assembly for a global *)];
+ (* Now come the MSVC declspec attributes *)
+ List.iter (fun a -> Hashtbl.add table a (AttrName true))
+ [ "thread"; "naked"; "dllimport"; "dllexport";
+ "selectany"; "allocate"; "nothrow"; "novtable"; "property";
+ "uuid"; "align" ];
+ List.iter (fun a -> Hashtbl.add table a (AttrFunType false))
+ [ "format"; "regparm"; "longcall"; "noinline"; "always_inline"; ];
+ List.iter (fun a -> Hashtbl.add table a (AttrFunType true))
+ [ "stdcall";"cdecl"; "fastcall"; "noreturn"];
+ List.iter (fun a -> Hashtbl.add table a AttrType)
+ ("mode" :: qualifier_attributes);
+ (* GCC label and statement attributes. *)
+ List.iter (fun a -> Hashtbl.add table a AttrStmt)
+ [ "hot"; "cold"; "fallthrough"; "assume"; "musttail" ];
+ table
+
+let register_attribute an ac =
+ if Hashtbl.mem attribute_hash an then begin
+ let pp fmt c =
+ match c with
+ | AttrName b -> Format.fprintf fmt "(AttrName %B)" b
+ | AttrFunType b -> Format.fprintf fmt "(AttrFunType %B)" b
+ | AttrType -> Format.fprintf fmt "AttrType"
+ | AttrIgnored -> Format.fprintf fmt "AttrIgnored"
+ | AttrStmt -> Format.fprintf fmt "AttrStmt"
+ in
+ Kernel.warning
+ "Replacing existing class for attribute %s: was %a, now %a"
+ an pp (Hashtbl.find attribute_hash an) pp ac
+ end;
+ Hashtbl.replace attribute_hash an ac
+
+let remove_attribute = Hashtbl.remove attribute_hash
+
+let get_attribute_class ~default name =
+ match Hashtbl.find attribute_hash name with
+ | exception Not_found -> default
+ | AttrIgnored -> default
+ | ac -> ac
+
+let is_known_attribute = Hashtbl.mem attribute_hash
+
+let partition_attributes
+ ~(default:attribute_class)
+ (attrs: attribute list) :
+ attribute list * attribute list * attribute list =
+ let rec loop (n,f,t) = function
+ [] -> n, f, t
+ | (Attr(an, _) | AttrAnnot an as a) :: rest ->
+ match get_attribute_class ~default an with
+ AttrName _ -> loop (add_attribute a n, f, t) rest
+ | AttrFunType _ ->
+ loop (n, add_attribute a f, t) rest
+ | AttrType -> loop (n, f, add_attribute a t) rest
+ | AttrStmt ->
+ Kernel.warning "unexpected statement attribute %s" an;
+ loop (n,f,t) rest
+ | AttrIgnored -> loop (n, f, t) rest
+ in
+ loop ([], [], []) attrs
+
+let split_storage_modifier al =
+ let isstoragemod (Attr(an, _) | AttrAnnot an : attribute) : bool =
+ try
+ match Hashtbl.find attribute_hash an with
+ | AttrName issm -> issm
+ | _ -> false
+ with Not_found -> false
+ in
+ let stom, rest = List.partition isstoragemod al in
+ if not (Machine.msvcMode ()) then stom, rest
+ else
+ (* Put back the declspec. Put it without the leading __ since these will
+ * be added later *)
+ let stom' =
+ List.map (fun a ->
+ match a with
+ | Attr(an, args) -> Attr("declspec", [ACons(an, args)])
+ | AttrAnnot _ -> assert false
+ ) stom
+ in
+ stom', rest
+
+let frama_c_ghost_else = "fc_ghost_else"
+let () = register_attribute frama_c_ghost_else (AttrStmt)
+
+let frama_c_ghost_formal = "fc_ghost_formal"
+let () = register_attribute frama_c_ghost_formal (AttrName false)
+
+let frama_c_init_obj = "fc_initialized_object"
+let () = register_attribute frama_c_init_obj (AttrName false)
+
+let frama_c_mutable = "fc_mutable"
+let () = register_attribute frama_c_mutable (AttrName false)
+
+let frama_c_inlined = "fc_inlined"
+let () = register_attribute frama_c_inlined (AttrFunType false)
+
+let () =
+ register_attribute bitfield_attribute_name AttrType;
+ register_attribute anonymous_attribute_name AttrIgnored;
+ List.iter
+ (fun a -> register_attribute a AttrIgnored)
+ fc_internal_attributes;
+ List.iter
+ (fun a -> register_attribute a AttrType)
+ cast_irrelevant_attributes
+
+let () =
+ Cil_datatype.drop_non_logic_attributes :=
+ drop_attributes spare_attributes_for_logic_cast
+
+let () =
+ Cil_datatype.drop_fc_internal_attributes :=
+ drop_attributes fc_internal_attributes
+
+let () =
+ Cil_datatype.drop_unknown_attributes :=
+ let is_annot_or_known_attr = function
+ | Attr (name, _) -> is_known_attribute name
+ (* Attribute annotations are always known. *)
+ | AttrAnnot _ -> true
+ in
+ (fun attributes ->
+ List.filter is_annot_or_known_attr attributes)
diff --git a/src/kernel_services/ast_queries/ast_attributes.mli b/src/kernel_services/ast_queries/ast_attributes.mli
new file mode 100644
index 0000000000000000000000000000000000000000..ea0eec9e476bc6a3af1eede6c8fbe57bd1051234
--- /dev/null
+++ b/src/kernel_services/ast_queries/ast_attributes.mli
@@ -0,0 +1,186 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2025 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** This file contains attribute related types/functions/values.
+ @since Frama-C+dev
+ @before Frama-C+dev Most of these functions were in {!Cil}
+*)
+
+open Cil_types
+
+(* **************************** *)
+(** {2 Attributes lists/values} *)
+(* **************************** *)
+
+(** Name of the attribute that is automatically inserted (with an [AINT size]
+ argument when querying the type of a field that is a bitfield.
+*)
+val bitfield_attribute_name : string
+
+(** Name of the attribute that is inserted when generating a name for a varinfo
+ representing an anonymous function parameter.
+*)
+val anonymous_attribute_name : string
+
+(** Attribute identifying anonymous function parameters. *)
+val anonymous_attribute : attribute
+
+(** [const], [volatile], [restrict] and [ghost] attributes. *)
+val qualifier_attributes : string list
+
+(** Internal attributes of Frama-C. *)
+val fc_internal_attributes : string list
+
+(** Qualifiers and internal attributes to remove when doing a C cast. *)
+val cast_irrelevant_attributes : string list
+
+(** Qualifiers and internal attributes to remove when doing a C cast. *)
+val spare_attributes_for_c_cast : string list
+
+(** Qualifiers and internal attributes to remove when doing a C cast. *)
+val spare_attributes_for_logic_cast : string list
+
+(** A block marked with this attribute is known to be a ghost else. *)
+val frama_c_ghost_else: string
+
+(** A varinfo marked with this attribute is known to be a ghost formal. *)
+val frama_c_ghost_formal: string
+
+(** a formal marked with this attribute is known to be a pointer to an
+ object being initialized by the current function, which can thus assign
+ any sub-object regardless of const status.
+*)
+val frama_c_init_obj: string
+
+(** a field struct marked with this attribute is known to be mutable, i.e.
+ it can be modified even on a const object.
+*)
+val frama_c_mutable: string
+
+(** A block marked with this attribute is known to be inlined, i.e.
+ it replaces a call to an inline function.
+*)
+val frama_c_inlined : string
+
+(* ***************************** *)
+(** {2 Attributes manipulations} *)
+(* ***************************** *)
+
+(** Returns the name of an attribute. *)
+val attribute_name : attribute -> string
+
+(** True if the named attribute appears in the attribute list. The list of
+ attributes must be sorted.
+*)
+val has_attribute : string -> attribute list -> bool
+
+(** Add an attribute. Maintains the attributes in sorted order of the second
+ argument. The attribute is not added if it is already there.
+*)
+val add_attribute : attribute -> attributes -> attribute list
+
+(** Add a list of attributes. Maintains the attributes in sorted order. The
+ second argument must be sorted, but not necessarily the first.
+*)
+val add_attributes : attribute list -> attributes -> attributes
+
+(** Remove all attributes with the given name. Maintains the attributes in
+ sorted order.
+*)
+val drop_attribute : string -> attributes -> attribute list
+
+(** Remove all attributes with names appearing in the string list.
+ Maintains the attributes in sorted order.
+*)
+val drop_attributes : string list -> attributes -> attributes
+
+(** Returns the list of parameters associated to an attribute. The list is empty
+ if there is no such attribute or it has no parameters at all.
+*)
+val find_attribute : string -> attribute list -> attrparam list
+
+(** Retains attributes with the given name *)
+val filter_attributes : string -> attribute list -> attribute list
+
+(** retains attributes corresponding to type qualifiers (6.7.3) *)
+val filter_qualifier_attributes : attribute list -> attribute list
+
+(** given some attributes on an array type, split them into those that belong
+ to the type of the elements of the array (currently, qualifiers such as
+ const and volatile), and those that must remain on the array, in that
+ order. *)
+val split_array_attributes : attribute list -> attribute list * attribute list
+
+(** Separate out the storage-modifier name attributes *)
+val split_storage_modifier: attribute list -> attribute list * attribute list
+
+(* **************************************** *)
+(** {2 Attributes classes and registration} *)
+(* **************************************** *)
+
+type attribute_class =
+ (** Attribute of a name. If argument is true and we are on MSVC then
+ the attribute is printed using __declspec as part of the storage
+ specifier *)
+ | AttrName of bool
+
+ (** Attribute of a function type. If argument is true and we are on
+ MSVC then the attribute is printed just before the function name *)
+ | AttrFunType of bool
+
+ (** Attribute of a type *)
+ | AttrType
+
+ (** Attribute of a statement or a block *)
+ | AttrStmt
+
+ (** Attribute that does not correspond to either of the above classes and is
+ ignored by functions {!get_attribute_class} and {!partition_attributes}. *)
+ | AttrIgnored
+
+(* Table containing all registered attributes. *)
+val attribute_hash : (string, attribute_class) Hashtbl.t
+
+(** Add a new attribute with a specified class *)
+val register_attribute : string -> attribute_class -> unit
+
+(** Remove an attribute previously registered. *)
+val remove_attribute : string -> unit
+
+(** Return the class of an attributes. The class `default' is returned for
+ unknown and ignored attributes.
+*)
+val get_attribute_class : default:attribute_class -> string -> attribute_class
+
+(** {!is_known_attribute attrname} returns true if the attribute named
+ {!attrname} is known by Frama-C.
+*)
+val is_known_attribute : string -> bool
+
+(** Partition the attributes into classes: name attributes, function type and
+ type attributes. Unknown and ignored attributes are returned in the
+ `default` attribute class.
+*)
+val partition_attributes : default:attribute_class -> attribute list ->
+ attribute list * (* AttrName *)
+ attribute list * (* AttrFunType *)
+ attribute list (* AttrType *)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index afb9866d1960c716ea147ca1c4905d68906931c9..344d7315ed71ba7ce4db326f5d19a600dea58763 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -56,6 +56,7 @@ open Logic_const
open Cil_datatype
open Cil_types
open Machine
+open Ast_attributes
(* ************************************************************************* *)
(* Reporting messages *)
@@ -145,102 +146,22 @@ let stmt_of_instr_list ?(loc=Location.unknown) = function
(**** Utility functions ******)
-(**** ATTRIBUTES ****)
-
-(* Attributes are added as they are (e.g. if we add ["__attr"] and then ["attr"] both are added).
- When checking for the presence of an attribute [x] or trying to remove it, underscores are
- removed at the beginning and the end of the attribute for both the [x] attribute and the
- attributes of the list. For example, if have a call:
-
- dropAttribute "__const" [ Attr("const", []) ; Attr("__const", []) ; Attr("__const__", []) ]
-
- The result is [].
-*)
-
-let bitfield_attribute_name = "FRAMA_C_BITFIELD_SIZE"
-
-let anonymous_attribute_name = "fc_anonymous"
-let anonymous_attribute = Attr(anonymous_attribute_name, [])
-
-(** Construct sorted lists of attributes ***)
-let attributeName =
- function Attr(a, _) | AttrAnnot a -> Extlib.strip_underscore a
-
-let addAttribute
- (Attr(an, _) | AttrAnnot an as a: attribute) (al: attributes) =
- let rec insertSorted = function
- [] -> [a]
- | ((Attr(an0, _) | AttrAnnot an0 as a0) :: rest) as l ->
- if an < an0 then a :: l
- else if Cil_datatype.Attribute.equal a a0 then l (* Do not add if already in there *)
- else a0 :: insertSorted rest (* Make sure we see all attributes with
- * this name *)
- in
- insertSorted al
-
-(** The second attribute list is sorted *)
-let addAttributes al0 (al: attributes) : attributes =
- if al0 == [] then al else
- List.fold_left (fun acc a -> addAttribute a acc) al al0
-
-let dropAttribute (an: string) (al: attributes) =
- let an = Extlib.strip_underscore an in
- List.filter (fun a -> attributeName a <> an) al
-
-let hasAttribute (an: string) (al: attribute list) : bool =
- let an = Extlib.strip_underscore an in
- List.exists (fun a -> attributeName a = an) al
-
-let rec dropAttributes (anl: string list) (al: attributes) =
- match al with
- | [] -> []
- | a :: q ->
- let q' = dropAttributes anl q in
- if List.mem (attributeName a) anl then
- q' (* drop this attribute *)
- else
- if q' == q then al (* preserve sharing *) else a :: q'
-
-let filterAttributes (an: string) (al: attribute list) : attribute list =
- let an = Extlib.strip_underscore an in
- List.filter (fun a -> attributeName a = an) al
-
-let findAttribute (an: string) (al: attribute list) : attrparam list =
- let an = Extlib.strip_underscore an in
- List.fold_left
- (fun acc -> function
- | Attr (_, param) as a0 when attributeName a0 = an -> param @ acc
- | _ -> acc)
- [] al
+(* Attributes *)
let rec typeAttrs { tnode; tattr } =
match tnode with
| TVoid -> tattr
| TInt _ -> tattr
| TFloat _ -> tattr
- | TNamed t -> addAttributes tattr (typeAttrs t.ttype)
+ | TNamed t -> add_attributes tattr (typeAttrs t.ttype)
| TPtr _ -> tattr
| TArray _ -> tattr
- | TComp comp -> addAttributes comp.cattr tattr
- | TEnum enum -> addAttributes enum.eattr tattr
+ | TComp comp -> add_attributes comp.cattr tattr
+ | TEnum enum -> add_attributes enum.eattr tattr
| TFun _ -> tattr
| TBuiltin_va_list -> tattr
-let qualifier_attributes = [ "const"; "restrict"; "volatile"; "ghost" ]
-
-let fc_internal_attributes = ["declspec"; "arraylen"; "fc_stdlib"]
-
-let cast_irrelevant_attributes = ["visibility"]
-
-let filter_qualifier_attributes al =
- List.filter
- (fun a -> List.mem (attributeName a) qualifier_attributes) al
-
-let splitArrayAttributes =
- List.partition
- (fun a -> List.mem (attributeName a) qualifier_attributes)
-
-let rec typeAddAttributes ?(combine=addAttributes) a0 t =
+let rec typeAddAttributes ?(combine=add_attributes) a0 t =
begin
match a0 with
| [] ->
@@ -260,9 +181,9 @@ let rec typeAddAttributes ?(combine=addAttributes) a0 t =
| TNamed _
| TBuiltin_va_list -> {t with tattr = add t.tattr}
| TArray (bt, l) ->
- let att_elt, att_typ = splitArrayAttributes a0 in
+ let att_elt, att_typ = split_array_attributes a0 in
let bt' = arrayPushAttributes att_elt bt in
- let tattr = addAttributes att_typ t.tattr in
+ let tattr = add_attributes att_typ t.tattr in
Cil_const.mk_tarray ~tattr bt' l
end
(* Push attributes that belong to the type of the elements of the array as
@@ -276,18 +197,18 @@ and arrayPushAttributes al t =
(**** Look for the presence of an attribute in a type ****)
-let typeHasAttribute attr typ = hasAttribute attr (typeAttrs typ)
+let typeHasAttribute attr typ = has_attribute attr (typeAttrs typ)
let rec typeHasQualifier attr t =
match t.tnode with
| TNamed ti ->
- hasAttribute attr t.tattr || typeHasQualifier attr ti.ttype
+ has_attribute attr t.tattr || typeHasQualifier attr ti.ttype
| TArray (bt, _) ->
- typeHasQualifier attr bt || (* ill-formed type *) hasAttribute attr t.tattr
- | _ -> hasAttribute attr (typeAttrs t)
+ typeHasQualifier attr bt || (* ill-formed type *) has_attribute attr t.tattr
+ | _ -> has_attribute attr (typeAttrs t)
let typeHasAttributeMemoryBlock a (ty:typ): bool =
- let f attrs = if hasAttribute a attrs then raise Exit in
+ let f attrs = if has_attribute a attrs then raise Exit in
let rec visit (t: typ) : unit =
f t.tattr;
match t.tnode with
@@ -320,7 +241,7 @@ let rec typeRemoveAttributes ?anl t =
let tattr =
match anl with
| None -> []
- | Some anl -> dropAttributes anl t.tattr
+ | Some anl -> drop_attributes anl t.tattr
in
let reshare () =
if tattr == t.tattr
@@ -351,7 +272,7 @@ let rec typeRemoveAttributesDeep (anl: string list) t =
(* Try to preserve sharing. We use sharing to be more efficient, but also
to detect that we have removed an attribute under typedefs *)
let reshare () =
- let tattr = dropAttributes anl t.tattr in
+ let tattr = drop_attributes anl t.tattr in
if tattr == t.tattr
then t
else Cil_const.mk_typ ~tattr t.tnode
@@ -364,12 +285,12 @@ let rec typeRemoveAttributesDeep (anl: string list) t =
| TPtr t ->
let t' = typeRemoveAttributesDeep anl t in
if t != t'
- then Cil_const.mk_tptr ~tattr:(dropAttributes anl t.tattr) t'
+ then Cil_const.mk_tptr ~tattr:(drop_attributes anl t.tattr) t'
else reshare ()
| TArray (t, l) ->
let t' = typeRemoveAttributesDeep anl t in
if t != t'
- then Cil_const.mk_tarray ~tattr:(dropAttributes anl t.tattr) t' l
+ then Cil_const.mk_tarray ~tattr:(drop_attributes anl t.tattr) t' l
else reshare ()
| TFun _ -> reshare ()
| TComp _ -> reshare ()
@@ -378,7 +299,7 @@ let rec typeRemoveAttributesDeep (anl: string list) t =
let tt = typeRemoveAttributesDeep anl ti.ttype in
if tt == ti.ttype
then reshare ()
- else typeAddAttributes (dropAttributes anl t.tattr) tt
+ else typeAddAttributes (drop_attributes anl t.tattr) tt
let type_remove_qualifier_attributes =
typeRemoveAttributes qualifier_attributes
@@ -386,126 +307,10 @@ let type_remove_qualifier_attributes =
let type_remove_qualifier_attributes_deep =
typeRemoveAttributesDeep qualifier_attributes
-type attributeClass =
- | AttrName of bool
- (* Attribute of a name. If argument is true and we are on MSVC then
- * the attribute is printed using __declspec as part of the storage
- * specifier *)
- | AttrFunType of bool
- (* Attribute of a function type. If argument is true and we are on
- * MSVC then the attribute is printed just before the function name *)
-
- | AttrType
- (* Attribute of a type *)
-
- | AttrStmt
- (* Attribute of a statement or block *)
-
- | AttrIgnored
- (** Attribute that does not correspond to either of the above classes. *)
-
-(* This table contains the mapping of predefined attributes to classes.
- * Extend this table with more attributes as you need. This table is used to
- * determine how to associate attributes with names or type during cabs2cil
- * conversion *)
-let attributeHash: (string, attributeClass) Hashtbl.t =
- let table = Hashtbl.create 13 in
- List.iter (fun a -> Hashtbl.add table a (AttrName false))
- [ "section"; "constructor"; "destructor"; "unused"; "used"; "weak";
- "no_instrument_function"; "alias"; "no_check_memory_usage";
- "exception"; "model"; (* "restrict"; *)
- "aconst"; "asm" (* Gcc uses this to specify the name to be used in
- * assembly for a global *)];
- (* Now come the MSVC declspec attributes *)
- List.iter (fun a -> Hashtbl.add table a (AttrName true))
- [ "thread"; "naked"; "dllimport"; "dllexport";
- "selectany"; "allocate"; "nothrow"; "novtable"; "property";
- "uuid"; "align" ];
- List.iter (fun a -> Hashtbl.add table a (AttrFunType false))
- [ "format"; "regparm"; "longcall"; "noinline"; "always_inline"; ];
- List.iter (fun a -> Hashtbl.add table a (AttrFunType true))
- [ "stdcall";"cdecl"; "fastcall"; "noreturn"];
- List.iter (fun a -> Hashtbl.add table a AttrType)
- ("mode" :: qualifier_attributes);
- (* GCC label and statement attributes. *)
- List.iter (fun a -> Hashtbl.add table a AttrStmt)
- [ "hot"; "cold"; "fallthrough"; "assume"; "musttail" ];
- table
-
-let isKnownAttribute = Hashtbl.mem attributeHash
-
-let attributeClass ~default name =
- match Hashtbl.find attributeHash name with
- | exception Not_found -> default
- | AttrIgnored -> default
- | ac -> ac
-
-let registerAttribute an ac =
- if Hashtbl.mem attributeHash an then begin
- let pp fmt c =
- match c with
- | AttrName b -> Format.fprintf fmt "(AttrName %B)" b
- | AttrFunType b -> Format.fprintf fmt "(AttrFunType %B)" b
- | AttrType -> Format.fprintf fmt "AttrType"
- | AttrIgnored -> Format.fprintf fmt "AttrIgnored"
- | AttrStmt -> Format.fprintf fmt "AttrStmt"
- in
- Kernel.warning
- "Replacing existing class for attribute %s: was %a, now %a"
- an pp (Hashtbl.find attributeHash an) pp ac
- end;
- Hashtbl.replace attributeHash an ac
-let removeAttribute = Hashtbl.remove attributeHash
-
-(** Partition the attributes into classes *)
-let partitionAttributes
- ~(default:attributeClass)
- (attrs: attribute list) :
- attribute list * attribute list * attribute list =
- let rec loop (n,f,t) = function
- [] -> n, f, t
- | (Attr(an, _) | AttrAnnot an as a) :: rest ->
- match attributeClass ~default an with
- AttrName _ -> loop (addAttribute a n, f, t) rest
- | AttrFunType _ ->
- loop (n, addAttribute a f, t) rest
- | AttrType -> loop (n, f, addAttribute a t) rest
- | AttrStmt ->
- Kernel.warning "unexpected statement attribute %s" an;
- loop (n,f,t) rest
- | AttrIgnored -> loop (n, f, t) rest
- in
- loop ([], [], []) attrs
-
-let frama_c_ghost_else = "fc_ghost_else"
-let () = registerAttribute frama_c_ghost_else (AttrStmt)
-
-let frama_c_ghost_formal = "fc_ghost_formal"
-let () = registerAttribute frama_c_ghost_formal (AttrName false)
-
-let frama_c_init_obj = "fc_initialized_object"
-let () = registerAttribute frama_c_init_obj (AttrName false)
-
-let frama_c_mutable = "fc_mutable"
-let () = registerAttribute frama_c_mutable (AttrName false)
-
-let frama_c_inlined = "fc_inlined"
-let () = registerAttribute frama_c_inlined (AttrFunType false)
-
-let () =
- registerAttribute bitfield_attribute_name AttrType;
- registerAttribute anonymous_attribute_name AttrIgnored;
- List.iter
- (fun a -> registerAttribute a AttrIgnored)
- fc_internal_attributes;
- List.iter
- (fun a -> registerAttribute a AttrType)
- cast_irrelevant_attributes
-
let unrollType (t: typ) : typ =
let rec withAttrs (al: attributes) (t: typ) : typ =
match t.tnode with
- | TNamed ti -> withAttrs (addAttributes al t.tattr) ti.ttype
+ | TNamed ti -> withAttrs (add_attributes al t.tattr) ti.ttype
| _ -> typeAddAttributes al t
in
withAttrs [] t
@@ -525,15 +330,15 @@ let rec unrollTypeSkel (t : typ) : typ_node =
let rec unrollTypeDeep (t: typ) : typ =
let rec withAttrs (al: attributes) (t: typ) : typ =
match t.tnode with
- | TNamed r -> withAttrs (addAttributes al t.tattr) r.ttype
+ | TNamed r -> withAttrs (add_attributes al t.tattr) r.ttype
| TPtr bt ->
let bt' = unrollTypeDeep bt in
- let tattr = addAttributes al t.tattr in
+ let tattr = add_attributes al t.tattr in
Cil_const.mk_tptr ~tattr bt'
| TArray (bt, l) ->
- let att_elt, att_typ = splitArrayAttributes al in
+ let att_elt, att_typ = split_array_attributes al in
let bt' = arrayPushAttributes att_elt (unrollTypeDeep bt) in
- let tattr = addAttributes att_typ t.tattr in
+ let tattr = add_attributes att_typ t.tattr in
Cil_const.mk_tarray ~tattr bt' l
| TFun (rt, args, isva) ->
let rt' = unrollTypeDeep rt in
@@ -543,14 +348,14 @@ let rec unrollTypeDeep (t: typ) : typ =
| Some argl ->
Some (List.map (fun (an, at, aa) -> (an, unrollTypeDeep at, aa)) argl)
in
- let tattr = addAttributes al t.tattr in
+ let tattr = add_attributes al t.tattr in
Cil_const.mk_tfun ~tattr rt' args' isva
| _ -> typeAddAttributes al t
in
withAttrs [] t
let is_ghost_else block =
- hasAttribute frama_c_ghost_else block.battrs
+ has_attribute frama_c_ghost_else block.battrs
let rec enforceGhostStmtCoherence ?(force_ghost=false) stmt =
let force_ghost = force_ghost || stmt.ghost in
@@ -630,10 +435,10 @@ let makeFormalsVarDecl ?ghost (n,t,a) =
vi
let isGhostFormalVarinfo vi =
- hasAttribute frama_c_ghost_formal vi.vattr
+ has_attribute frama_c_ghost_formal vi.vattr
let isGhostFormalVarDecl (_name, _type, attr) =
- hasAttribute frama_c_ghost_formal attr
+ has_attribute frama_c_ghost_formal attr
let setFormalsDecl vi typ =
match unrollTypeSkel typ with
@@ -641,7 +446,7 @@ let setFormalsDecl vi typ =
let is_ghost d = vi.vghost || isGhostFormalVarDecl d in
let makeFormalsVarDecl i (n,t,a as x) =
let x = if n = "" then begin
- let a = addAttribute anonymous_attribute a in
+ let a = add_attribute anonymous_attribute a in
"__x" ^ string_of_int i,t,a
end
else x
@@ -1112,19 +917,19 @@ let transient_block b =
"ignoring request to mark transient a block with local variables:@\n%a"
Cil_datatype.Block.pretty b
end else
- b.battrs <- addAttribute (Attr (vis_tmp_attr,[])) b.battrs; b
+ b.battrs <- add_attribute (Attr (vis_tmp_attr,[])) b.battrs; b
let block_of_transient b =
- if hasAttribute vis_tmp_attr b.battrs then begin
+ if has_attribute vis_tmp_attr b.battrs then begin
if b.blocals <> [] then
Kernel.fatal
"Block that is supposed to be transient declares local variabels";
- b.battrs <- dropAttribute vis_tmp_attr b.battrs;
+ b.battrs <- drop_attribute vis_tmp_attr b.battrs;
b.bscoping <- false
end;
b
-let is_transient_block b = hasAttribute vis_tmp_attr b.battrs
+let is_transient_block b = has_attribute vis_tmp_attr b.battrs
let flatten_transient_sub_blocks b =
let prev = ref None in
@@ -2228,7 +2033,7 @@ and visitCilStmt (vis:cilVisitor) (s: stmt) : stmt =
let make i = mkStmt ~ghost:res.ghost (Instr i) in
let last = mkStmt ~ghost:res.ghost res.skind in
let block = mkBlockNonScoping (List.map make instr_list @ [ last ]) in
- block.battrs <- addAttribute (Attr (vis_tmp_attr, [])) block.battrs;
+ block.battrs <- add_attribute (Attr (vis_tmp_attr, [])) block.battrs;
(* Make our statement contain the instructions to prepend *)
res.skind <- Block block;
vis#pop_stmt s; res
@@ -2248,7 +2053,7 @@ and childrenStmt (toPrepend: instr list ref) (vis:cilVisitor) (s:stmt): stmt =
(function (stmt,modified,writes,reads,calls) as orig->
let stmt' = visitCilStmt vis stmt in
(match stmt'.skind with
- | Block b -> b.battrs <- dropAttribute vis_tmp_attr b.battrs;
+ | Block b -> b.battrs <- drop_attribute vis_tmp_attr b.battrs;
| _ -> ());
(* might make sense for the default to be
to just copy the varinfo when using the copy visitor,
@@ -2497,7 +2302,7 @@ and visitCilAttributes (vis: cilVisitor) (al: attribute list) : attribute list=
id vis#vattr childrenAttribute) al in
if al' != al then
(* Must re-sort *)
- addAttributes al' []
+ add_attributes al' []
else
al
and childrenAttribute (vis: cilVisitor) (a: attribute) : attribute =
@@ -3234,29 +3039,6 @@ let rec stripCasts (e: exp) =
let rec stripTermCasts (t: term) =
match t.term_node with TCast(_,_, t') -> stripTermCasts t' | _ -> t
-(* Separate out the storage-modifier name attributes *)
-let separateStorageModifiers (al: attribute list) =
- let isstoragemod (Attr(an, _) | AttrAnnot an : attribute) : bool =
- try
- match Hashtbl.find attributeHash an with
- | AttrName issm -> issm
- | _ -> false
- with Not_found -> false
- in
- let stom, rest = List.partition isstoragemod al in
- if not (msvcMode ()) then stom, rest
- else
- (* Put back the declspec. Put it without the leading __ since these will
- * be added later *)
- let stom' =
- List.map
- (function
- | Attr(an, args) -> Attr("declspec", [ACons(an, args)])
- | AttrAnnot _ -> assert false)
- stom
- in
- stom', rest
-
let isVoidType t =
match unrollTypeSkel t with
| TVoid -> true
@@ -3295,7 +3077,7 @@ let isCharPtrType t =
let isCharConstPtrType t =
match unrollType t with
| { tnode = TPtr tau; tattr } when isCharType tau ->
- hasAttribute "const" tattr
+ has_attribute "const" tattr
| _ -> false
let isIntegralType t =
@@ -3566,8 +3348,8 @@ and typeOffset basetyp = function
is still const (except potentially a mutable subsubpart, etc.)
*)
let attrs =
- if hasAttribute frama_c_mutable fi.fattr then
- dropAttribute "const" attrs
+ if has_attribute frama_c_mutable fi.fattr then
+ drop_attribute "const" attrs
else attrs
in
typeOffset (typeAddAttributes attrs fi.ftype) o
@@ -3614,7 +3396,7 @@ let rec typeOfTermLval = function
and typeTermOffset basetyp =
let blendAttributes baseAttrs t =
let (_, _, contagious) =
- partitionAttributes ~default:(AttrName false) baseAttrs in
+ partition_attributes ~default:(AttrName false) baseAttrs in
let rec putAttributes = function
| Ctype typ ->
Ctype (typeAddAttributes contagious typ)
@@ -3915,11 +3697,11 @@ let rec bytesAlignOf t =
differently when put into a struct, or in each of its fields.
*)
and alignOfField (fi: fieldinfo) =
- let fieldIsPacked = hasAttribute "packed" fi.fattr
- || hasAttribute "packed" fi.fcomp.cattr
+ let fieldIsPacked = has_attribute "packed" fi.fattr
+ || has_attribute "packed" fi.fcomp.cattr
in
if fieldIsPacked then begin
- if hasAttribute "aligned" fi.fattr then
+ if has_attribute "aligned" fi.fattr then
(* field is packed and aligned => process alignment *)
let field_alignment = process_aligned_attribute ~may_reduce:true
(fun fmt -> Format.fprintf fmt "field %s" fi.fname)
@@ -3988,7 +3770,7 @@ and process_aligned_attribute (pp:Format.formatter->unit) ~may_reduce attrs defa
be specified as well. When used as part of a typedef, the aligned attribute
can both increase and decrease alignment, and specifying the packed
attribute generates a warning." *)
- match filterAttributes "aligned" attrs with
+ match filter_attributes "aligned" attrs with
| [] ->
(* no __aligned__ attribute, so get the default alignment *)
default_align ()
@@ -4432,7 +4214,7 @@ and constFold (machdep: bool) (e: exp) : exp =
let t' = unrollType t in
match e.enode, t'.tnode with
| Const (CInt64(i,_k,_)), (TInt nk | TEnum {ekind = nk})
- when dropAttributes fc_internal_attributes t'.tattr = [] ->
+ when drop_attributes fc_internal_attributes t'.tattr = [] ->
begin
(* If the cast has attributes, leave it alone. *)
Kernel.debug ~dkey "ConstFold to %a : %a@."
@@ -4684,7 +4466,7 @@ and constFoldToInt ?(machdep=true) e =
let bitsSizeOfBitfield typlv =
match unrollType typlv with
| { tnode = TInt _; tattr } | { tnode = TEnum _; tattr } as t ->
- (match findAttribute bitfield_attribute_name tattr with
+ (match find_attribute bitfield_attribute_name tattr with
| [AInt i] -> Integer.to_int_exn i
| _ -> bitsSizeOf t)
| t -> bitsSizeOf t
@@ -4803,9 +4585,6 @@ let mk_behavior ?(name=default_behavior_name) ?(assumes=[]) ?(requires=[])
b_extended = extended;
}
-let spare_attributes_for_c_cast =
- fc_internal_attributes @ qualifier_attributes
-
let type_remove_attributes_for_c_cast t =
let attributes_to_remove =
fc_internal_attributes @ cast_irrelevant_attributes
@@ -4813,9 +4592,6 @@ let type_remove_attributes_for_c_cast t =
let t = typeRemoveAttributesDeep attributes_to_remove t in
typeRemoveAttributes spare_attributes_for_c_cast t
-let spare_attributes_for_logic_cast =
- spare_attributes_for_c_cast
-
let type_remove_attributes_for_logic_type t =
let attributes_to_remove =
fc_internal_attributes @ cast_irrelevant_attributes
@@ -4823,22 +4599,6 @@ let type_remove_attributes_for_logic_type t =
let t = typeRemoveAttributesDeep attributes_to_remove t in
typeRemoveAttributes spare_attributes_for_logic_cast t
-let () = Cil_datatype.drop_non_logic_attributes :=
- dropAttributes spare_attributes_for_logic_cast
-
-let () = Cil_datatype.drop_fc_internal_attributes :=
- dropAttributes fc_internal_attributes
-
-let () =
- Cil_datatype.drop_unknown_attributes :=
- let is_annot_or_known_attr = function
- | Attr (name, _) -> isKnownAttribute name
- (* Attribute annotations are always known. *)
- | AttrAnnot _ -> true
- in
- (fun attributes ->
- List.filter is_annot_or_known_attr attributes)
-
let need_cast ?(force=false) oldt newt =
let oldt = type_remove_attributes_for_c_cast (unrollType oldt) in
let newt = type_remove_attributes_for_c_cast (unrollType newt) in
@@ -4967,7 +4727,7 @@ let makeFormalVar fdec ?(ghost=fdec.svar.vghost) ?(where = "$") ?loc name typ :
let makeit name =
let vi = makeLocal ~ghost ?loc ~formal:true fdec name typ in
if ghost && not fdec.svar.vghost then
- vi.vattr <- addAttribute (Attr(frama_c_ghost_formal, [])) vi.vattr ;
+ vi.vattr <- add_attribute (Attr(frama_c_ghost_formal, [])) vi.vattr ;
vi
in
let error () = Kernel.fatal ~current:true
@@ -5342,8 +5102,8 @@ let global_attributes = function
| GAsm _ | GText _ -> []
let is_in_libc attrs =
- hasAttribute "fc_stdlib" attrs ||
- hasAttribute "fc_stdlib_generated" attrs
+ has_attribute "fc_stdlib" attrs ||
+ has_attribute "fc_stdlib_generated" attrs
let global_is_in_libc g =
is_in_libc (global_attributes g)
@@ -5585,7 +5345,7 @@ let argsToPairOfLists args =
(argsToList args)
let remove_attributes_for_integral_promotion a =
- dropAttributes (bitfield_attribute_name :: spare_attributes_for_c_cast) a
+ drop_attributes (bitfield_attribute_name :: spare_attributes_for_c_cast) a
let rec integralPromotion t = (* c.f. ISO 6.3.1.1 *)
let open Cil_const in
@@ -5601,7 +5361,7 @@ let rec integralPromotion t = (* c.f. ISO 6.3.1.1 *)
let k = if isSigned IChar then ISChar else IUChar in
integralPromotion (mk_tint ~tattr k)
| { tnode = TInt k; tattr } ->
- begin match findAttribute bitfield_attribute_name tattr with
+ begin match find_attribute bitfield_attribute_name tattr with
| [AInt size] ->
(* This attribute always fits in int. *)
let size = Integer.to_int_exn size in
@@ -5828,10 +5588,10 @@ let qualifier_context_ptr = function
let included_qualifiers ?(context=Identical) a1 a2 =
let a1 = filter_qualifier_attributes a1 in
let a2 = filter_qualifier_attributes a2 in
- let a1 = dropAttribute "restrict" a1 in
- let a2 = dropAttribute "restrict" a2 in
- let a1_no_cv = dropAttributes ["const"; "volatile"] a1 in
- let a2_no_cv = dropAttributes ["const"; "volatile"] a2 in
+ let a1 = drop_attribute "restrict" a1 in
+ let a2 = drop_attribute "restrict" a2 in
+ let a1_no_cv = drop_attributes ["const"; "volatile"] a1 in
+ let a2_no_cv = drop_attributes ["const"; "volatile"] a2 in
let is_equal = Cil_datatype.Attributes.equal a1 a2 in
if is_equal then true
else begin
@@ -5920,7 +5680,7 @@ type combineWhat =
let combineAttributes what olda a =
match what with
| CombineFunarg _ -> a (* override old attributes with new ones *)
- | _ -> addAttributes olda a (* union of attributes *)
+ | _ -> add_attributes olda a (* union of attributes *)
type combineFunction =
{
@@ -6107,19 +5867,19 @@ let combineTypesGen ?emitwith (combF : combineFunction)
combF.typ_combine combF
~strictInteger ~strictReturnTypes what ot at
in
- let a = addAttributes oa aa in
+ let a = add_attributes oa aa in
(n, t, a))
oldargslist argslist)
in
(* Drop missingproto as soon as one of the type is a properly declared one*)
let olda' =
- if not (hasAttribute "missingproto" t.tattr) then
- dropAttribute "missingproto" oldt.tattr
+ if not (has_attribute "missingproto" t.tattr) then
+ drop_attribute "missingproto" oldt.tattr
else oldt.tattr
in
let a' =
- if not (hasAttribute "missingproto" oldt.tattr) then
- dropAttribute "missingproto" t.tattr
+ if not (has_attribute "missingproto" oldt.tattr) then
+ drop_attribute "missingproto" t.tattr
else t.tattr
in
let tattr = combineAttributes what olda' a' in
@@ -6875,7 +6635,7 @@ let is_mutable (lhost, offset) =
match typ'.tnode, off with
| _, NoOffset -> can_mutate
| _, Field (fi, off) ->
- let can_mutate = can_mutate || hasAttribute frama_c_mutable fi.fattr in
+ let can_mutate = can_mutate || has_attribute frama_c_mutable fi.fattr in
aux can_mutate fi.ftype off
| TArray (typ, _), Index(_, off) -> aux can_mutate typ off
| _, Index _ ->
@@ -6893,7 +6653,7 @@ let rec is_initialized_aux on_same_obj e =
and is_initialized_lhost on_same_obj lhost =
match lhost with
- | Var vi -> hasAttribute frama_c_init_obj vi.vattr
+ | Var vi -> has_attribute frama_c_init_obj vi.vattr
| Mem e -> on_same_obj && is_initialized_aux false e
let is_initialized e =
@@ -7332,11 +7092,11 @@ let create_alpha_renaming old_args new_args =
List.iter2
(fun old_vi new_vi ->
Hashtbl.add conversion old_vi.vid new_vi;
- if hasAttribute anonymous_attribute_name new_vi.vattr &&
- not (hasAttribute anonymous_attribute_name old_vi.vattr)
+ if has_attribute anonymous_attribute_name new_vi.vattr &&
+ not (has_attribute anonymous_attribute_name old_vi.vattr)
then begin
new_vi.vname <- old_vi.vname;
- new_vi.vattr <- dropAttribute anonymous_attribute_name new_vi.vattr;
+ new_vi.vattr <- drop_attribute anonymous_attribute_name new_vi.vattr;
end;
match old_vi.vlogic_var_assoc, new_vi.vlogic_var_assoc with
| None, _ -> () (* nothing to convert in logic spec. *)
@@ -7455,3 +7215,71 @@ let typeDeepDropAllAttributes t =
let typeAttr { tattr } = tattr
let setTypeAttrs t tattr = { t with tattr }
+
+(* **************************** *)
+(* Forward attributes functions *)
+(* **************************** *)
+
+let bitfield_attribute_name = bitfield_attribute_name
+
+let anonymous_attribute_name = anonymous_attribute_name
+
+let anonymous_attribute = anonymous_attribute
+
+let frama_c_ghost_else = frama_c_ghost_else
+
+let frama_c_ghost_formal = frama_c_ghost_formal
+
+let frama_c_init_obj = frama_c_init_obj
+
+let frama_c_mutable = frama_c_mutable
+
+let frama_c_inlined = frama_c_inlined
+
+let attributeName = attribute_name
+
+let hasAttribute = has_attribute
+
+let addAttribute = add_attribute
+
+let addAttributes = add_attributes
+
+let dropAttribute = drop_attribute
+
+let dropAttributes = drop_attributes
+
+let findAttribute = find_attribute
+
+let filterAttributes = filter_attributes
+
+let filter_qualifier_attributes = filter_qualifier_attributes
+
+let splitArrayAttributes = split_array_attributes
+
+type attributeClass =
+ AttrName of bool
+ (** Attribute of a name. If argument is true and we are on MSVC then
+ the attribute is printed using __declspec as part of the storage
+ specifier *)
+ | AttrFunType of bool
+ (** Attribute of a function type. If argument is true and we are on
+ MSVC then the attribute is printed just before the function name *)
+ | AttrType
+ (** Attribute of a type *)
+ | AttrStmt
+ (** Attribute of a statement or a block *)
+ | AttrIgnored
+ (** Attribute that does not correspond to either of the above classes and is
+ ignored by functions [attributeClass] and [partitionAttributes]. *)
+
+let registerAttribute = register_attribute
+
+let removeAttribute = remove_attribute
+
+let attributeClass = get_attribute_class
+
+let isKnownAttribute = is_known_attribute
+
+let partitionAttributes = partition_attributes
+
+let separateStorageModifiers = split_storage_modifier
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index dc33546920994bbc45115aa49b8c4bb9e8c65693..c52cee769465a3584839a71f1e01036039edf749 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -339,9 +339,6 @@ val unrollTypeNode: typ -> typ_node
types. Will collect all attributes *)
val unrollTypeDeep: typ -> typ
-(** Separate out the storage-modifier name attributes *)
-val separateStorageModifiers: attribute list -> attribute list * attribute list
-
(** returns the type of the result of an arithmetic operator applied to
values of the corresponding input types.
@since Nitrogen-20111001 (moved from Cabs2cil)
@@ -1322,101 +1319,6 @@ val instr_falls_through : instr -> bool
(** {2 Values for manipulating attributes} *)
(* ************************************************************************* *)
-(** Various classes of attributes
- @before 30.0-Zinc [AttrStmt] and [AttrIgnored] didn't exist
-*)
-type attributeClass =
- AttrName of bool
- (** Attribute of a name. If argument is true and we are on MSVC then
- the attribute is printed using __declspec as part of the storage
- specifier *)
- | AttrFunType of bool
- (** Attribute of a function type. If argument is true and we are on
- MSVC then the attribute is printed just before the function name *)
- | AttrType
- (** Attribute of a type *)
- | AttrStmt
- (** Attribute of a statement or a block *)
- | AttrIgnored
- (** Attribute that does not correspond to either of the above classes and is
- ignored by functions [attributeClass] and [partitionAttributes]. *)
-
-val registerAttribute: string -> attributeClass -> unit
-(** Add a new attribute with a specified class *)
-
-val removeAttribute: string -> unit
-(** Remove an attribute previously registered. *)
-
-val isKnownAttribute: string -> bool
-(** [isKnownAttribute attrname] returns true if the attribute named [attrname]
- is known by Frama-C.
- @since 30.0-Zinc
-*)
-
-val attributeClass: default:attributeClass -> string -> attributeClass
-(** Return the class of an attributes. The class `default' is returned for
- unknown and ignored attributes.
- @before 30.0-Zinc no [default] argument
-*)
-
-(** Partition the attributes into classes: name attributes, function type and
- type attributes. Unknown and ignored attributes are returned in the
- `default` attribute class.
- @before 30.0-Zinc no [default] argument
-*)
-val partitionAttributes: default:attributeClass ->
- attributes -> attribute list * (* AttrName *)
- attribute list * (* AttrFunType *)
- attribute list (* AttrType *)
-
-(** Add an attribute. Maintains the attributes in sorted order of the second
- argument. The attribute is not added if it is already there. *)
-val addAttribute: attribute -> attributes -> attributes
-
-(** Add a list of attributes. Maintains the attributes in sorted order. The
- second argument must be sorted, but not necessarily the first *)
-val addAttributes: attribute list -> attributes -> attributes
-
-(** Remove all attributes with the given name. Maintains the attributes in
- sorted order. *)
-val dropAttribute: string -> attributes -> attributes
-
-(** Remove all attributes with names appearing in the string list.
- Maintains the attributes in sorted order *)
-val dropAttributes: string list -> attributes -> attributes
-
-(** A block marked with this attribute is known to be a ghost else.
-
- @since 21.0-Scandium
-*)
-val frama_c_ghost_else: string
-
-(** A varinfo marked with this attribute is known to be a ghost formal.
-
- @since 20.0-Calcium
-*)
-val frama_c_ghost_formal: string
-
-(** a formal marked with this attribute is known to be a pointer to an
- object being initialized by the current function, which can thus assign
- any sub-object regardless of const status.
-
- @since 18.0-Argon
-*)
-val frama_c_init_obj: string
-
-(** a field struct marked with this attribute is known to be mutable, i.e.
- it can be modified even on a const object.
-
- @since 18.0-Argon
-*)
-val frama_c_mutable: string
-
-(** A block marked with this attribute is known to be inlined, i.e.
- it replaces a call to an inline function.
-*)
-val frama_c_inlined: string
-
(** [true] if the underlying left-value of the given expression is allowed to be
assigned to thanks to a [frama_c_init_obj] attribute. *)
val is_initialized: exp -> bool
@@ -1438,7 +1340,6 @@ val isGhostFormalVarinfo: varinfo -> bool
*)
val isGhostFormalVarDecl: (string * typ * attributes) -> bool
-
(** [true] iff the given variable is a const global variable with non extern
storage.
@@ -1452,20 +1353,6 @@ val isGlobalInitConst: varinfo -> bool
*)
val typeDeepDropAllAttributes: typ -> typ
-(** Retains attributes with the given name *)
-val filterAttributes: string -> attributes -> attributes
-
-(** True if the named attribute appears in the attribute list. The list of
- attributes must be sorted. *)
-val hasAttribute: string -> attributes -> bool
-
-(** Returns the name of an attribute. *)
-val attributeName: attribute -> string
-
-(** Returns the list of parameters associated to an attribute. The list is empty if there
- is no such attribute or it has no parameters at all. *)
-val findAttribute: string -> attribute list -> attrparam list
-
(** Returns all the attributes contained in a type. This requires a traversal
of the type structure, in case of composite, enumeration and named types *)
val typeAttrs: typ -> attribute list
@@ -1545,31 +1432,6 @@ val type_remove_attributes_for_c_cast: typ -> typ
*)
val type_remove_attributes_for_logic_type: typ -> typ
-(** retains attributes corresponding to type qualifiers (6.7.3) *)
-val filter_qualifier_attributes: attributes -> attributes
-
-(** given some attributes on an array type, split them into those that belong
- to the type of the elements of the array (currently, qualifiers such as
- const and volatile), and those that must remain on the array, in that
- order
- @since Oxygen-20120901 *)
-val splitArrayAttributes: attributes -> attributes * attributes
-
-val bitfield_attribute_name: string
-(** Name of the attribute that is automatically inserted (with an [AINT size]
- argument when querying the type of a field that is a bitfield *)
-
-val anonymous_attribute_name: string
-(** Name of the attribute that is inserted when generating a name for a varinfo
- representing an anonymous function parameter.
- @since 24.0-Chromium
-*)
-
-val anonymous_attribute: attribute
-(** attribute identifying anonymous function parameters
- @since 24.0-Chromium
-*)
-
(** Convert an expression into an attrparam, if possible. Otherwise raise
NotAnAttrParam with the offending subexpression *)
val expToAttrParam: exp -> attrparam
@@ -2463,6 +2325,10 @@ val set_extension_handler:
@before 30.0-Zinc This function did not take a [plugin:string] parameter
*)
+(* ************************************************************************* *)
+(** {2 Deprecated types functions} *)
+(* ************************************************************************* *)
+
(** Returns the attributes of a type.
@deprecated Frama-C+dev *)
val typeAttr: typ -> attribute list
@@ -2474,8 +2340,169 @@ val typeAttr: typ -> attribute list
val setTypeAttrs: typ -> attributes -> typ
[@@alert deprecated "Use [{t with tattr = ...}] instead."]
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
+(* ************************************************************************* *)
+(** {2 Deprecated values moved to Ast_attributes} *)
+(* ************************************************************************* *)
+
+val bitfield_attribute_name: string
+(** Name of the attribute that is automatically inserted (with an [AINT size]
+ argument when querying the type of a field that is a bitfield.
+*)
+[@@deprecated "Use Ast_attributes.bitfield_attribute_name instead."]
+
+val anonymous_attribute_name: string
+(** Name of the attribute that is inserted when generating a name for a varinfo
+ representing an anonymous function parameter.
+ @since 24.0-Chromium
+*)
+[@@deprecated "Use Ast_attributes.anonymous_attribute_name instead."]
+
+val anonymous_attribute: attribute
+(** attribute identifying anonymous function parameters
+ @since 24.0-Chromium
+*)
+[@@deprecated "Use Ast_attributes.anonymous_attribute instead."]
+
+(** Returns the name of an attribute. *)
+val attributeName: attribute -> string
+[@@deprecated "Use Ast_attributes.attribute_name instead."]
+
+(** True if the named attribute appears in the attribute list. The list of
+ attributes must be sorted. *)
+val hasAttribute: string -> attributes -> bool
+[@@deprecated "Use Ast_attributes.has_attribute instead."]
+
+(** Add an attribute. Maintains the attributes in sorted order of the second
+ argument. The attribute is not added if it is already there. *)
+val addAttribute: attribute -> attributes -> attributes
+[@@deprecated "Use Ast_attributes.add_attribute instead."]
+
+(** Add a list of attributes. Maintains the attributes in sorted order. The
+ second argument must be sorted, but not necessarily the first *)
+val addAttributes: attribute list -> attributes -> attributes
+[@@deprecated "Use Ast_attributes.add_attributes instead."]
+
+(** Remove all attributes with the given name. Maintains the attributes in
+ sorted order. *)
+val dropAttribute: string -> attributes -> attributes
+[@@deprecated "Use Ast_attributes.drop_attribute instead."]
+
+(** Remove all attributes with names appearing in the string list.
+ Maintains the attributes in sorted order *)
+val dropAttributes: string list -> attributes -> attributes
+[@@deprecated "Use Ast_attributes.drop_attributes instead."]
+
+(** Returns the list of parameters associated to an attribute. The list is empty if there
+ is no such attribute or it has no parameters at all. *)
+val findAttribute: string -> attribute list -> attrparam list
+[@@deprecated "Use Ast_attributes.find_attribute instead."]
+
+(** Retains attributes with the given name *)
+val filterAttributes: string -> attributes -> attributes
+[@@deprecated "Use Ast_attributes.filter_attributes instead."]
+
+(** retains attributes corresponding to type qualifiers (6.7.3) *)
+val filter_qualifier_attributes: attributes -> attributes
+[@@deprecated "Use Ast_attributes.filter_qualifier_attributes instead."]
+
+(** given some attributes on an array type, split them into those that belong
+ to the type of the elements of the array (currently, qualifiers such as
+ const and volatile), and those that must remain on the array, in that
+ order
+ @since Oxygen-20120901 *)
+val splitArrayAttributes: attributes -> attributes * attributes
+[@@deprecated "Use Ast_attributes.split_array_attributes instead."]
+
+(** Various classes of attributes
+ @before 30.0-Zinc [AttrStmt] and [AttrIgnored] didn't exist
+*)
+type attributeClass =
+ AttrName of bool
+ (** Attribute of a name. If argument is true and we are on MSVC then
+ the attribute is printed using __declspec as part of the storage
+ specifier *)
+ | AttrFunType of bool
+ (** Attribute of a function type. If argument is true and we are on
+ MSVC then the attribute is printed just before the function name *)
+ | AttrType
+ (** Attribute of a type *)
+ | AttrStmt
+ (** Attribute of a statement or a block *)
+ | AttrIgnored
+ (** Attribute that does not correspond to either of the above classes and is
+ ignored by functions [attributeClass] and [partitionAttributes]. *)
+[@@deprecated "Use Ast_attributes.attribute_class instead."]
+
+val registerAttribute: string -> Ast_attributes.attribute_class -> unit
+(** Add a new attribute with a specified class *)
+[@@deprecated "Use Ast_attributes.register_attribute instead."]
+
+val removeAttribute: string -> unit
+(** Remove an attribute previously registered. *)
+[@@deprecated "Use Ast_attributes.remove_attribute instead."]
+
+val attributeClass: default:Ast_attributes.attribute_class -> string -> Ast_attributes.attribute_class
+(** Return the class of an attributes. The class `default' is returned for
+ unknown and ignored attributes.
+ @before 30.0-Zinc no [default] argument
+*)
+[@@deprecated "Use Ast_attributes.get_attribute_class instead."]
+
+val isKnownAttribute: string -> bool
+(** [isKnownAttribute attrname] returns true if the attribute named [attrname]
+ is known by Frama-C.
+ @since 30.0-Zinc
+*)
+[@@deprecated "Use Ast_attributes.is_known_attribute instead."]
+
+(** Partition the attributes into classes: name attributes, function type and
+ type attributes. Unknown and ignored attributes are returned in the
+ `default` attribute class.
+ @before 30.0-Zinc no [default] argument
+*)
+val partitionAttributes: default:Ast_attributes.attribute_class ->
+ attributes -> attribute list * (* AttrName *)
+ attribute list * (* AttrFunType *)
+ attribute list (* AttrType *)
+[@@deprecated "Use Ast_attributes.partition_attributes instead."]
+
+(** Separate out the storage-modifier name attributes *)
+val separateStorageModifiers: attribute list -> attribute list * attribute list
+[@@deprecated "Use Ast_attributes.split_storage_modifier instead."]
+
+(** A block marked with this attribute is known to be a ghost else.
+
+ @since 21.0-Scandium
+*)
+val frama_c_ghost_else: string
+[@@deprecated "Use Ast_attributes.frama_c_ghost_else instead."]
+
+(** A varinfo marked with this attribute is known to be a ghost formal.
+
+ @since 20.0-Calcium
+*)
+val frama_c_ghost_formal: string
+[@@deprecated "Use Ast_attributes.frama_c_ghost_formal instead."]
+
+(** a formal marked with this attribute is known to be a pointer to an
+ object being initialized by the current function, which can thus assign
+ any sub-object regardless of const status.
+
+ @since 18.0-Argon
*)
+val frama_c_init_obj: string
+[@@deprecated "Use Ast_attributes.frama_c_init_obj instead."]
+
+(** a field struct marked with this attribute is known to be mutable, i.e.
+ it can be modified even on a const object.
+
+ @since 18.0-Argon
+*)
+val frama_c_mutable: string
+[@@deprecated "Use Ast_attributes.frama_c_mutable instead."]
+
+(** A block marked with this attribute is known to be inlined, i.e.
+ it replaces a call to an inline function.
+*)
+val frama_c_inlined: string
+[@@deprecated "Use Ast_attributes.frama_c_inlined instead."]