Partager via

Annotations des structs et des classes

Vous pouvez annoter les membres de struct et de classe à l’aide d’annotations qui agissent comme des invariants. Elles sont supposées être vraies à tout appel de fonction ou entrée/sortie de fonction qui implique la structure englobante en tant que paramètre ou valeur de résultat.

Annotations de struct et de classe

  • _Field_range_(low, high)

    Le champ se trouve dans la plage (inclusive) de low à high. Équivalent à appliqué à l’objet annoté à _Satisfies_(_Curr_ >= low && _Curr_ <= high) l’aide des conditions préalables ou post appropriées.

  • _Field_size_(size), , _Field_size_opt_(size)_Field_size_bytes_(size), ,_Field_size_bytes_opt_(size)

    Champ qui a une taille accessible en écriture dans les éléments (ou octets) comme spécifié par size.

  • _Field_size_part_(size, count), , _Field_size_part_opt_(size, count)_Field_size_bytes_part_(size, count), ,_Field_size_bytes_part_opt_(size, count)

    Champ qui a une taille accessible en écriture dans les éléments (ou octets) comme spécifié par size, et les count éléments (octets) lisibles.

  • _Field_size_full_(size), , _Field_size_full_opt_(size)_Field_size_bytes_full_(size), ,_Field_size_bytes_full_opt_(size)

    Champ qui a à la fois une taille lisible et accessible en écriture dans des éléments (ou octets) comme spécifié par size.

  • _Field_z_

    Champ qui a une chaîne terminée par null.

  • _Struct_size_bytes_(size)

    S’applique à la déclaration de struct ou de classe. Indique qu’un objet valide de ce type peut être supérieur au type déclaré, avec le nombre d’octets spécifié par size. Par exemple :

    typedef _Struct_size_bytes_(nSize)
struct MyStruct {
    size_t nSize;
    ...
};

    La taille de la mémoire tampon en octets d’un paramètre pM de type MyStruct * est ensuite prise comme suit :

    min(pM->nSize, sizeof(MyStruct))

Exemple

#include <sal.h>

// This _Struct_size_bytes_ is equivalent to what below _Field_size_ means.
_Struct_size_bytes_(__builtin_offsetof(MyBuffer, buffer) + bufferSize * sizeof(int))
struct MyBuffer
{
    static int MaxBufferSize;

    _Field_z_
    const char* name;

    int firstField;

    // ... other fields

    _Field_range_(1, MaxBufferSize)
    int bufferSize;

    _Field_size_(bufferSize)        // Preferred way - easier to read and maintain.
    int buffer[]; // Using C99 Flexible array member
};

Remarques pour cet exemple :

  • _Field_z_ est équivalent à _Null_terminated_. _Field_z_ pour le champ de nom spécifie que le champ de nom est une chaîne terminée par null.
  • _Field_range_ pour bufferSize spécifier que la valeur de bufferSize doit être comprise dans 1 et MaxBufferSize (à la fois inclusive).
  • Les résultats finaux des annotations et _Struct_size_bytes_ des _Field_size_ annotations sont équivalents. Pour les structures ou classes qui ont une disposition similaire, _Field_size_ il est plus facile de lire et de gérer, car il a moins de références et de calculs que l’annotation équivalente _Struct_size_bytes_ . _Field_size_ ne nécessite pas de conversion en taille d’octet. Si la taille d’octet est la seule option, par exemple, pour un champ de pointeur void, _Field_size_bytes_ peut être utilisée. S’il existe à la fois, _Struct_size_bytes_ les deux _Field_size_ seront disponibles pour les outils. Il incombe à l’outil de faire si les deux annotations ne sont pas d’accord.

Voir aussi

  • Last updated on