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 qualifier_attributes : string list

const, volatile, restrict and ghost 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.

val anonymous_attribute : Cil_types.attribute

Attribute identifying anonymous function parameters.

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.

val frama_c_keep_block : string

Name of the attribute inserted by the elaboration to prevent user blocks from disappearing. It can be removed whenever block contracts have been processed.

val frama_c_destructor : string

Name of the attribute used to store the function that should be called when the corresponding variable exits its scope.

val fc_local_static : string

Name of the attribute used to indicate that a given static variable has a local syntactic scope (despite a global lifetime).

val fc_stdlib : string

Internal attribute use in Frama-C's libc, see share/libc/feature.h.

val fc_stdlib_generated : string

Attribute added when generating variadic functions from Frama-C's libc.

val fc_oldstyleproto : string

Attribute added by Frama-C's parser.

val fc_missingproto : string

Attribute added by cabs2cil on functions calls encountered before any declaration/definition.

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. | AttrUnknown
type attribute_info = {
  1. attr_class : attribute_class;
    (*

    Class of the attribute.

    *)
  2. attr_ignore : bool;
    (*

    Ignore the attribute when comparing types.

    *)
  3. attr_print : bool;
    (*

    Print the attribute when printing the AST.

    *)
}

Registered informations about an attribute.

val known_table : (string, attribute_info) Stdlib.Hashtbl.t

Table containing all registered attributes.

val register : ?print:bool -> ?ignore:bool -> attribute_class -> string -> unit

Add a new attribute with a specified class, if it should be printed (default is true) and ignore when comparing types (default if true for AttrUnknown class and false otherwise).

val register_noprint : ?ignore:bool -> attribute_class -> string -> unit

Same as register but with print set to false.

val register_list : ?print:bool -> ?ignore:bool -> attribute_class -> string list -> unit

Call register on a list of attributes with the same class and print status.

val remove : string -> unit

Remove an attribute previously registered.

val is_known : string -> bool

is_known attrname returns true if the attribute named attrname is known (registered) by Frama-C.

val find_known : string -> attribute_info option

find_known attrname returns Some attrinfo if the attribute named attrname is known (registered) by Frama-C, None otherwise.

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 should_print : string -> bool

should_print attrname return the field attr_print of the attribute named attrname if it is known (registered) by Frama-C, and return true otherwise.

val should_ignore : string -> bool

should_ignore attrname return the field attr_ignore of the attribute named attrname if it is known (registered) by Frama-C, and return false otherwise.

Partition the attributes into classes: name, function type and type. Statement attributes are removed with a warning, Unknown attributes are returned in the `default` attribute class. If this class is AttrUnknown, again, they are removed like AttrStmt without warning.

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