Megosztás a következőn keresztül:


Struktúrák és osztályok annotálása

A struktúrák és az osztálytagok annotálhatók olyan annotációkkal, amelyek invariánsként működnek – ezek feltételezhetően igazak bármely függvényhívás alkalmával vagy függvény belépésénél/kilépésénél, ahol a struktúrát paraméterként vagy visszatérési értékként használják.

Szerkezet- és osztályjegyzetek

  • _Field_range_(low, high)

    A mező a low és high közötti tartományon belül van, beleértve az értékeket is. Egyenértékű a _Satisfies_(_Curr_ >= low && _Curr_ <= high) jegyzetekkel ellátott objektumra a megfelelő elő- vagy utófeltételek használatával.

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

    Olyan mező, amelynek írható mérete az elemekben (vagy bájtokban) a megadottak szerint sizevan megadva.

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

    Olyan mező, amelynek mérete elemekben (vagy bájtokban) az alapján írható, ahogyan az a size van meghatározva, valamint amely count elemek (bájtok) olvashatóak.

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

    Olyan mező, amely az size által megadott elemekben (vagy bájtokban) olvasható és írható méretű.

  • _Field_z_

    Null értékű sztringgel rendelkező mező.

  • _Struct_size_bytes_(size)

    A szerkezetre vagy osztálydeklarációra vonatkozik. Azt jelzi, hogy egy érvényes objektum ebből a típusból nagyobb lehet a deklarált típusnál, a bájtok számát pedig a megadott size határozza meg. Például:

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

    A paraméter pM bájtban kifejezett puffer mérete a MyStruct * típushoz a következő:

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

példa

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

A példához tartozó megjegyzések:

  • _Field_z_egyenértékű a .-nak._Null_terminated_ _Field_z_ mező azt jelzi, hogy a név egy nullával lezárt karakterlánc.
  • _Field_range_ a bufferSize beállítás azt határozza meg, hogy az értéknek bufferSize az 1-es és MaxBufferSize a (mindkettőt is magában foglaló) értéken belül kell lennie.
  • A széljegyzetek és _Struct_size_bytes_ a _Field_size_ széljegyzetek végeredménye egyenértékű. A hasonló elrendezésű _Field_size_ struktúrák vagy osztályok könnyebben olvashatók és karbantarthatók, mivel kevesebb hivatkozással és számítással rendelkezik, mint a megfelelő _Struct_size_bytes_ széljegyzet. _Field_size_ nincs szükség a bájtméretre való átalakításra. Ha a bájtméret az egyetlen lehetőség, például üres mutató mező esetén használható _Field_size_bytes_ . Ha mind a _Struct_size_bytes_ és a _Field_size_ létezik, mindkettő elérhető lesz az eszközök számára. Az eszközön múlik, hogy mi a teendő, ha a két jelölés nem egyezik meg.

Lásd még