Annotazioni di struct e classi

  • Articolo

È possibile annotare i membri struct e di classe utilizzando le annotazioni che operano come invarianti, si presume che siano true per qualsiasi chiamata di funzione o entrata/uscita di funzione che include la struttura contenitore come parametro o valore restituito.

Annotazioni di struct e classi

  • _Field_range_(low, high)

    Il campo si trova nell'intervallo (incluso) da low a high. Equivalente ad applicare _Satisfies_(_Curr_ >= low && _Curr_ <= high) all'oggetto annotato utilizzando le pre/postcondizioni appropriate.

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

    Campo con una dimensione scrivibile in elementi (o byte) come specificato da 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)

    Campo con una dimensione scrivibile in elementi (o byte) come specificato da size e count degli elementi (byte) che sono leggibili.

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

    Campo che contiene sia dimensione leggibile che modificabile in elementi (o byte) come specificato da size.

  • _Field_z_

    Campo con terminazione Null.

  • _Struct_size_bytes_(size)

    Si applica alla dichiarazione di struct o classe. Indica che un oggetto valido di tale tipo può essere maggiore rispetto al tipo dichiarato, con il numero di byte specificati da size. Ad esempio:

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

    Le dimensioni del buffer in byte di un parametro pM di tipo MyStruct * vengono quindi prese in modo che siano:

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

Esempio

#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
};

Note per questo esempio:

  • _Field_z_ è pari a _Null_terminated_. _Field_z_ per il campo name specifica che il campo name è una stringa con terminazione Null.
  • _Field_range_ per bufferSize specifica che il valore di bufferSize deve essere compreso tra 1 e MaxBufferSize (inclusi entrambi).
  • I risultati finali delle _Struct_size_bytes_ annotazioni e _Field_size_ sono equivalenti. Per le strutture o le classi con un layout simile, _Field_size_ è più facile da leggere e gestire, perché include meno riferimenti e calcoli rispetto all'annotazione equivalente _Struct_size_bytes_ . _Field_size_ non richiede la conversione alle dimensioni dei byte. Se la dimensione dei byte è l'unica opzione, ad esempio, per un campo puntatore void, _Field_size_bytes_ può essere utilizzata. Se esistono entrambi _Struct_size_bytes_ , _Field_size_ entrambi saranno disponibili per gli strumenti. Spetta allo strumento cosa fare se le due annotazioni non sono d'accordo.

Vedi anche