通过

批注结构和类

可以使用行为与不变量类似的注释来批注结构和类成员，在任何涉及将封闭结构作为参数或结果值的函数调用或函数入口/出口中，假定这些成员为 true。

结构和类批注

  • _Field_range_(low, high)

    该字段的范围为 low 到 high（含）。 等效于通过使用适当的前提条件或后置条件应用于带批注对象的 _Satisfies_(_Curr_ >= low && _Curr_ <= high)。

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

    其元素（或字节）具有由 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)

    其元素（或字节）具有由 size 指定的可写大小，且这些元素（或字节）的 count 可读的字段。

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

    其元素（或字节）具有由 size 指定的可读和可写大小的字段。

  • _Field_z_

    具有以 null 结尾的字符串的字段。

  • _Struct_size_bytes_(size)

    适用于结构或类声明。 指示该类型的有效对象可能大于声明类型的有效对象，字节数由 size 指定。 例如：

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

    pM 类型的 MyStruct * 参数的缓冲区大小（以字节为单位）则为：

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

示例

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

此示例的备注：

  • _Field_z_ 等效于 _Null_terminated_。 名称字段的 _Field_z_ 指定名称字段是一个以 null 结尾的字符串。
  • _Field_range_ 的 bufferSize 指定 bufferSize 的值应在 1 到 MaxBufferSize 之间（含这两个值）。
  • _Struct_size_bytes_ 和 _Field_size_ 注释的最终结果等效。 对于有相似布局的结构或类，_Field_size_ 更容易读取和维护，因为它的引用和计算比等效 _Struct_size_bytes_ 注释少。 _Field_size_ 不需要转换为字节大小。 如果字节大小是唯一的选项，（例如，对于 void 指针字段）可以使用 _Field_size_bytes_。 如果 _Struct_size_bytes_ 和 _Field_size_ 都存在，则它们都可用于工具。 如果两个注释不一致，由工具决定所用注释。

另请参阅