package frama-c

  1. Overview
  2. Docs
Platform dedicated to the analysis of source code written in C

Install 

dune-project
 Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

  1. M
    Michele Alberti
  2. T
    Thibaud Antignac
  3. G
    Gergö Barany
  4. P
    Patrick Baudin
  5. N
    Nicolas Bellec
  6. T
    Thibaut Benjamin
  7. A
    Allan Blanchard
  8. L
    Lionel Blatter
  9. F
    François Bobot
  10. R
    Richard Bonichon
  11. V
    Vincent Botbol
  12. Q
    Quentin Bouillaguet
  13. D
    David Bühler
  14. Z
    Zakaria Chihani
  15. S
    Sylvain Chiron
  16. L
    Loïc Correnson
  17. J
    Julien Crétin
  18. P
    Pascal Cuoq
  19. Z
    Zaynah Dargaye
  20. B
    Basile Desloges
  21. J
    Jean-Christophe Filliâtre
  22. P
    Philippe Herrmann
  23. M
    Maxime Jacquemin
  24. B
    Benjamin Jorge
  25. F
    Florent Kirchner
  26. A
    Alexander Kogtenkov
  27. R
    Remi Lazarini
  28. T
    Tristan Le Gall
  29. K
    Kilyan Le Gallic
  30. J
    Jean-Christophe Léchenet
  31. M
    Matthieu Lemerre
  32. D
    Dara Ly
  33. D
    David Maison
  34. C
    Claude Marché
  35. A
    André Maroneze
  36. T
    Thibault Martin
  37. F
    Fonenantsoa Maurica
  38. M
    Melody Méaulle
  39. B
    Benjamin Monate
  40. Y
    Yannick Moy
  41. P
    Pierre Nigron
  42. A
    Anne Pacalet
  43. V
    Valentin Perrelle
  44. G
    Guillaume Petiot
  45. D
    Dario Pinto
  46. V
    Virgile Prevosto
  47. A
    Armand Puccetti
  48. F
    Félix Ridoux
  49. V
    Virgile Robles
  50. J
    Jan Rochel
  51. M
    Muriel Roger
  52. C
    Cécile Ruet-Cros
  53. J
    Julien Signoles
  54. N
    Nicolas Stouls
  55. K
    Kostyantyn Vorobyov
  56. B
    Boris Yakobowski

Maintainers

  1. F
    frama-ci-bot@frama-c.com

Sources

frama-c-31.0-beta-Gallium.tar.gz
sha256=095ffbb3086a6cd963a03e3defab4f0dc32e9a43f026e552ec9ae346a6e20522

doc/frama-c.kernel/Frama_c_kernel/Ast_attributes/index.html

Module Frama_c_kernel.Ast_attributes

This file contains attribute related types/functions/values.

  • since 31.0-Gallium
  • before 31.0-Gallium

    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) 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