Rediger

Del via

Annotating Structs and Classes

You can annotate struct and class members by using annotations that act like invariants—they are presumed to be true at any function call or function entry/exit that involves the enclosing structure as a parameter or a result value.

Struct and Class Annotations

  • _Field_range_(low, high)

    The field is in the range (inclusive) from low to high. Equivalent to _Satisfies_(_Curr_ >= low && _Curr_ <= high) applied to the annotated object by using the appropriate pre or post conditions.

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

    A field that has a writable size in elements (or bytes) as specified by 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)

    A field that has a writable size in elements (or bytes) as specified by size, and the count of those elements (bytes) that are readable.

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

    A field that has both readable and writable size in elements (or bytes) as specified by size.

  • _Field_z_

    A field that has a null-terminated string.

  • _Struct_size_bytes_(size)

    Applies to struct or class declaration. Indicates that a valid object of that type may be larger than the declared type, with the number of bytes being specified by size. For example:

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

    The buffer size in bytes of a parameter pM of type MyStruct * is then taken to be:

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

Example

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

Notes for this example:

  • _Field_z_ is equivalent to _Null_terminated_. _Field_z_ for the name field specifies that the name field is a null-terminated string.
  • _Field_range_ for bufferSize specifies that the value of bufferSize should be within 1 and MaxBufferSize (both inclusive).
  • The end results of the _Struct_size_bytes_ and _Field_size_ annotations are equivalent. For structures or classes that have a similar layout, _Field_size_ is easier to read and maintain, because it has fewer references and calculations than the equivalent _Struct_size_bytes_ annotation. _Field_size_ doesn't require conversion to the byte size. If byte size is the only option, for example, for a void pointer field, _Field_size_bytes_ can be used. If both _Struct_size_bytes_ and _Field_size_ exist, both will be available to tools. It is up to the tool what to do if the two annotations disagree.

See also

  • Last updated on