Sdílet prostřednictvím

Zadávání poznámek ke strukturám a třídám

  • Článek

Pomocí poznámek, které fungují jako invarianty, můžete přidávat poznámky– předpokládá se, že mají hodnotu true při jakémkoli volání funkce nebo vstupu nebo výstupu funkce, která zahrnuje uzavřenou strukturu jako parametr nebo výslednou hodnotu.

Poznámky ke strukturám a třídám

  • _Field_range_(low, high)

    Pole je v oblasti (včetně) od low do high. Ekvivalentní použití _Satisfies_(_Curr_ >= low && _Curr_ <= high) u anotovaného objektu pomocí odpovídajících podmínek před nebo po.

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

    Pole, které má zapisovatelnou velikost v prvcích (nebo bajtech), jak je určeno 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)

    Pole, které má zapisovatelnou velikost v prvcích (nebo bajtech), jak sizeje určeno , a count těch prvků (bajty), které jsou čitelné.

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

    Pole, které má čitelné i zapisovatelné velikosti v prvcích (nebo bajtech), jak je určeno size.

  • _Field_z_

    Pole s řetězcem ukončeným hodnotou null.

  • _Struct_size_bytes_(size)

    Platí pro deklaraci struktury nebo třídy. Označuje, že platný objekt tohoto typu může být větší než deklarovaný typ s počtem bajtů, které sizejsou určeny . Příklad:

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

    Velikost vyrovnávací paměti v bajtech parametru pM typu MyStruct * se pak provede takto:

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

Příklad

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

Poznámky pro tento příklad:

  • _Field_z_ je ekvivalent _Null_terminated_. _Field_z_ Pro pole názvu určuje, že pole názvu je řetězec ukončený hodnotou null.
  • _Field_range_ určuje bufferSize , že hodnota by měla být v rozsahu bufferSize 1 i MaxBufferSize (včetně).
  • Koncové výsledky _Struct_size_bytes_ a _Field_size_ poznámky jsou ekvivalentní. U struktur nebo tříd, které mají podobné rozložení, _Field_size_ je snadnější číst a udržovat, protože má méně odkazů a výpočtů než ekvivalentní _Struct_size_bytes_ poznámka. _Field_size_ nevyžaduje převod na velikost bajtu. Pokud je velikost bajtu jedinou možností, například pro pole ukazatele void, _Field_size_bytes_ lze použít. Pokud obojí _Struct_size_bytes_ i _Field_size_ existuje, budou obě nástroje k dispozici. Je na nástroji, co dělat, pokud dvě poznámky nesouhlasí.

Viz také