Bagikan melalui

Membuat Anotasi Structs dan Classes

Anda dapat membuat anotasi struct dan anggota kelas dengan menggunakan anotasi yang bertindak seperti invariants—mereka dianggap benar pada panggilan fungsi atau entri/keluar fungsi apa pun yang melibatkan struktur penutup sebagai parameter atau nilai hasil.

Anotasi Struktur dan Kelas

  • _Field_range_(low, high)

    Bidang berada dalam rentang (inklusif) dari low ke high. Setara dengan _Satisfies_(_Curr_ >= low && _Curr_ <= high) diterapkan ke objek yang dianotasikan dengan menggunakan kondisi pra atau posting yang sesuai.

  • _Field_size_(size), , _Field_size_opt_(size)_Field_size_bytes_(size),_Field_size_bytes_opt_(size)

    Bidang yang memiliki ukuran bisa-tulis dalam elemen (atau byte) seperti yang ditentukan oleh 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)

    Bidang yang memiliki ukuran bisa-tulis dalam elemen (atau byte) seperti yang ditentukan oleh size, dan count elemen tersebut (byte) yang dapat dibaca.

  • _Field_size_full_(size), , _Field_size_full_opt_(size)_Field_size_bytes_full_(size),_Field_size_bytes_full_opt_(size)

    Bidang yang memiliki ukuran yang dapat dibaca dan dapat ditulis dalam elemen (atau byte) seperti yang ditentukan oleh size.

  • _Field_z_

    Bidang yang memiliki string null-terminated.

  • _Struct_size_bytes_(size)

    Berlaku untuk struct atau deklarasi kelas. Menunjukkan bahwa objek yang valid dari jenis tersebut mungkin lebih besar dari jenis yang dideklarasikan, dengan jumlah byte yang ditentukan oleh size. Contohnya:

    typedef _Struct_size_bytes_(nSize)
struct MyStruct {
    size_t nSize;
    ...
};

    Ukuran buffer dalam byte dari parameter pM jenis MyStruct * kemudian diambil untuk menjadi:

    min(pM->nSize, sizeof(MyStruct))

Contoh

#include <sal.h>

// This _Struct_size_bytes_ is equivalent to what below _Field_size_ means.
_Struct_size_bytes_(__builtin_offsetof(MyBuffer, buffer) + bufferSize * sizeof(int))
struct MyBuffer
{
    static int MaxBufferSize;

    _Field_z_
    const char* name;

    int firstField;

    // ... other fields

    _Field_range_(1, MaxBufferSize)
    int bufferSize;

    _Field_size_(bufferSize)        // Preferred way - easier to read and maintain.
    int buffer[]; // Using C99 Flexible array member
};

Catatan untuk contoh ini:

  • _Field_z_ setara dengan _Null_terminated_. _Field_z_ untuk bidang nama menentukan bahwa bidang nama adalah string yang dihentikan null.
  • _Field_range_ untuk bufferSize menentukan bahwa nilai bufferSize harus dalam 1 dan MaxBufferSize (keduanya inklusif).
  • Hasil akhir anotasi _Struct_size_bytes_ dan _Field_size_ setara. Untuk struktur atau kelas yang memiliki tata letak serupa, _Field_size_ lebih mudah dibaca dan dikelola, karena memiliki lebih sedikit referensi dan perhitungan daripada anotasi yang setara _Struct_size_bytes_ . _Field_size_ tidak memerlukan konversi ke ukuran byte. Jika ukuran byte adalah satu-satunya opsi, misalnya, untuk bidang penunjuk yang batal, _Field_size_bytes_ dapat digunakan. Jika keduanya _Struct_size_bytes_ dan _Field_size_ ada, keduanya akan tersedia untuk alat. Terserah alat apa yang harus dilakukan jika kedua anotasi tidak setuju.

Lihat juga