Frama-C:
Plug-ins:
Libraries:

Frama-C API - Ast_attributes

This file contains attribute related types/functions/values.

  • since Frama-C+dev
  • before Frama-C+dev

    Most of these functions were in Cil

Attributes lists/values

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.

val anonymous_attribute : Cil_types.attribute

Attribute identifying anonymous function parameters.

val qualifier_attributes : string list

const, volatile, restrict and ghost attributes.

val fc_internal_attributes : string list

Internal attributes of Frama-C.

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

Qualifiers and internal attributes to remove when doing a C cast.

val frama_c_ghost_else : string

A block marked with this attribute is known to be a ghost else.

val frama_c_ghost_formal : string

A varinfo marked with this attribute is known to be a ghost formal.

val frama_c_init_obj : 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_mutable : 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_inlined : string

A block marked with this attribute is known to be inlined, i.e. it replaces a call to an inline function.

Attributes manipulations

val get_name : Cil_types.attribute -> string

Return the name of an attribute.

Add an attribute. Maintains the attributes in sorted order of the second argument. The attribute is not added if it is already there.

Add a list of attributes. Maintains the attributes in sorted order. The second argument must be sorted, but not necessarily the first.

Remove all attributes with the given name. Maintains the attributes in sorted order.

val drop_list : string list -> Cil_types.attributes -> Cil_types.attributes

Remove all attributes with names appearing in the string list. Maintains the attributes in sorted order.

val replace_params : string -> Cil_types.attrparam list -> Cil_types.attributes -> Cil_types.attributes

replace_params name params al will drop all the attributes named name in al and add a new attribute (name, params) in the list.

val contains : string -> Cil_types.attributes -> bool

True if the named attribute appears in the attribute list. The list of attributes must be sorted.

val find_params : string -> Cil_types.attributes -> Cil_types.attrparam list

Return 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 filter : string -> Cil_types.attributes -> Cil_types.attributes

Retain attributes with the given name.

Attributes classes and registration

type attribute_class =
  1. | AttrName of bool
  2. | AttrFunType of bool
  3. | AttrType
  4. | AttrStmt
  5. | AttrIgnored
val known_table : (string, attribute_class) Stdlib.Hashtbl.t

Table containing all registered attributes.

val register : attribute_class -> string -> unit

Add a new attribute with a specified class

val register_list : attribute_class -> string list -> unit

Register a list of attributes with a given class.

val remove : string -> unit

Remove an attribute previously registered.

val get_class : default:attribute_class -> string -> attribute_class

Return the class of an attribute. The class `default' is returned for unknown and ignored attributes.

val is_known : string -> bool

is_known_attribute attrname returns true if the attribute named attrname is known by Frama-C.

Partition the attributes into classes: name attributes, function type and type attributes. Unknown and ignored attributes are returned in the `default` attribute class.

Utility functions

val filter_qualifiers : Cil_types.attributes -> Cil_types.attributes

Retain attributes corresponding to type qualifiers (6.7.3)

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.

Separate out the storage-modifier name attributes