註釋結構和類別
您可以標註結構和類別成員使用動作的附註,如不變更它們是假設為 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 的位元組會接受如下:
|