Annotazioni di struct e classi
È possibile annotare struct e membri di una classe utilizzando annotazioni che operano come invarianti—si presume che siano vere a qualsiasi chiamata di funzione o ad ogni entrata/uscita da una funzione che include la struttura contenitore come parametro o un valore restituito.
Annotazioni di classe e struct
Annotazione |
Descrizione |
|---|---|
_Field_range_(low, high) |
Il campo si trova nell'intervallo che va da low a high (inclusi). Equivalente ad applicare _Satisfies_(_Curr_ >= low && _Curr_ <= high) all'oggetto annotato utilizzando le pre e post condizioni appropriate. |
_Field_size_(size) _Field_size_opt_(size) _Field_size_bytes_(size) _Field_size_bytes_opt_(size) |
Un campo con una dimensione scrivibile in elementi (o in byte) come specificato da 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) |
Un campo con una dimensione scrivibile in elementi (o in byte) come specificato da size e count degli elementi (byte) che sono leggibili. |
_Field_size_full_(size) _Field_size_full_opt_(size) _Field_size_bytes_full_(size) _Field_size_bytes_full_opt_(size) |
Un campo che contiene sia dimensione leggibile che modificabile in elementi (o in byte) come specificato da size. |
_Struct_size_bytes_(size) |
Si applica alle dichiarazioni di struct o classi. Indica che un oggetto valido di tale tipo può essere maggiore rispetto al tipo dichiarato, con il numero di byte specificati da size. Di seguito è riportato un esempio. La dimensione in byte del buffer di un parametro pM di tipo MyStruct * è presa da: |
Vedere anche
Riferimenti
Annotazione di parametri di funzione e valori restituiti
Annotazione del comportamento delle funzioni
Annotazione del comportamento di blocco
Specificare dove e quando applicare un'annotazione
Concetti
Altre risorse
Utilizzo delle annotazioni SAL per ridurre gli errori del codice C/C++