Funzioni intrinseche

  • Articolo

Un'espressione in SAL può essere un'espressione C/C++ a condizione che sia un'espressione che non produca effetti collaterali, ad esempio ++, -- e le chiamate di funzione hanno effetti collaterali in questo contesto. Tuttavia, SAL fornisce alcuni oggetti simili a funzioni e alcuni simboli riservati che possono essere usati nelle espressioni SAL. Queste funzioni sono definite funzioni intrinseche.

Utilizzo generico

Le seguenti annotazioni di funzioni intrinseche forniscono l'utilità generale per SAL.

Annotazione Descrizione
_Curr_ Sinonimo dell'oggetto attualmente annotato. Quando viene utilizzata l'annotazione _At_, _Curr_ è identica al primo parametro di _At_. In caso contrario, è il parametro o l'intera funzione/valore restituito con cui l'annotazione è lessicalmente associata.
_Inexpressible_(expr) Esprime una situazione in cui la dimensione di un buffer è troppo complessa per essere rappresentata con un'espressione di annotazione, ad esempio quando viene calcolata esaminando un set di dati di input e successivamente contando i membri selezionati.
_Nullterm_length_(param) param è il numero di elementi nel buffer fino a ma non include un carattere di terminazione Null. Può essere applicato a qualsiasi buffer di tipo non aggregato e non void.
_Old_(expr) Una volta valutato nella precondizione, _Old_ restituisce il valore di input expr. Una volta valutato nella post condizione, restituisce il valore expr come sarebbe stato valutato nella precondizione.
_Param_(n) Il nparametro th di una funzione, contando da 1 a ned n è una costante integrale letterale. Se il parametro è denominato, questa annotazione è identica all'accesso al parametro in base al nome. Nota: n può fare riferimento ai parametri posizionali definiti da puntini di sospensione oppure possono essere usati nei prototipi di funzione in cui i nomi non vengono usati.
return La parola chiave return riservata C/C++ può essere usata in un'espressione SAL per indicare il valore restituito di una funzione. Il valore è disponibile solo nello stato di post; è un errore di sintassi utilizzarlo in uno stato di pre.

Specifica della stringa

Le seguenti annotazioni di funzioni intrinseche abilitano la modifica delle stringhe. Tutte e quattro queste funzioni presentano lo stesso scopo: restituire il numero di elementi del tipo trovati prima di un terminatore null. Le differenze sono i tipi di dati negli elementi a cui fanno riferimento. Si noti che se si desidera specificare la lunghezza del buffer con terminazione null che non è composto da caratteri, utilizzare l'annotazione di _Nullterm_length_(param) dalla sezione precedente.

Annotazione Descrizione
_String_length_(param) param è il numero di elementi nella stringa fino a ma non include un carattere di terminazione Null. Questa annotazione è riservata ai tipi stringa di caratteri.
strlen(param) param è il numero di elementi nella stringa fino a ma non include un carattere di terminazione Null. Questa annotazione è riservata per l'uso su matrici di caratteri e assomiglia alla funzione di runtime C strlen().This annotation is reserved for use on character arrays and resembles the C Runtime function strlen().
wcslen(param) param è il numero di elementi nella stringa fino a (ma non incluso) un carattere di terminazione Null. Questa annotazione è riservata per l'uso su matrici di caratteri wide e assomiglia alla funzione di runtime C wcslen().This annotation is reserved for use on wide character arrays and resembles the C Runtime function wcslen().

Vedi anche