可以批注结构,并使用操作的批注的选件类成员,如对于它们将假定为 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 的字节然后将采用:
|