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
Annotation |
Description |
---|---|
_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. |
_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:
The buffer size in bytes of a parameter pM of type MyStruct * is then taken to be:
|
See Also
Reference
Annotating Function Parameters and Return Values
Specifying When and Where an Annotation Applies
Best Practices and Examples (SAL)