構造体とクラスに注釈を付ける
構造体注釈を付けて、不変条件がすべての関数呼び出しに当てはまると予想される動作し、開始フックと終了は、パラメーターまたは戻り値として囲む構造体を含める機能するようにコメントを使用してメンバーを並べ替えることができます。
構造体とクラスのコメント
注釈 |
説明 |
|---|---|
_Field_range_(low, high) |
フィールドは low から highでスコープ内に (包括) です。_Satisfies_(_Curr_ >= low && _Curr_ <= high) に相当は、注釈先オブジェクトに対応するまたは Post 条件を前に使用することで適用しました。 |
_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 バイトのバッファー サイズは次のように記述するために取得されます: |