可以批注结构和类的成员使用操作的说明,为固定被假定为 true 或在函数输入退出/涉及中的结构作为参数传递或结果值的所有函数调用。
结构和类批注
| 批注 | 说明 | 
|---|---|
| _Field_range_(low, high) | 字段在范围 (包含) 从 low 更改为 high。通过使用适当 Pre 或 Post 条件,等效于 _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。 | 
| _Struct_size_bytes_(size) | 适用于结构或类声明。指示该类型有效对象可能比声明的类型大,size可能指定的字节数。例如: 缓冲区大小为 MyStruct * 类型参数 pM 的字节然后采用为:  |