[Kernel] New attributes module, deprecate most of Cil attributes related functions

src/kernel_services/ast_queries/ast_attributes.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  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)

src/kernel_services/ast_queries/ast_attributes.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  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 *)

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."]