Intrinsic Functions
An expression in SAL can be a C/C++ expression provided that it is an expression that does not have side effects—for example, ++, --, and function calls all have side effects in this context. However, SAL does provide some function-like objects and some reserved symbols that can be used in SAL expressions. These are referred to as intrinsic functions.
General Purpose
The following instrinsic function annotations provide general utility for SAL.
| Annotation | Description |
|---|---|
_Curr_ |
A synonym for the object that is currently being annotated. When the _At_ annotation is in use, _Curr_ is the same as the first parameter to _At_. Otherwise, it is the parameter or the entire function/return value with which the annotation is lexically associated. |
_Inexpressible_(expr) |
Expresses a situation where the size of a buffer is too complex to represent by using an annotation expression—for example, when it is computed by scanning an input data set and then counting selected members. |
_Nullterm_length_(param) |
param is the number of elements in the buffer up to but not including a null terminator. It may be applied to any buffer of non-aggregate, non-void type. |
_Old_(expr) |
When it is evaluated in precondition, _Old_ returns the input value expr. When it is evaluated in post-condition, it returns the value expr as it would have been evaluated in precondition. |
_Param_(n) |
The nth parameter to a function, counting from 1 to n, and n is a literal integral constant. If the parameter is named, this annotation is identical to accessing the parameter by name. Note: n may refer to the positional parameters that are defined by an ellipsis, or may be used in function prototypes where names are not used. |
return |
The C/C++ reserved keyword return can be used in a SAL expression to indicate the return value of a function. The value is only available in post state; it is a syntax error to use it in pre state. |
String Specific
The following intrinsic function annotations enable manipulation of strings. All four of these functions serve the same purpose: to return the number of elements of the type that is found before a null terminator. The differences are the kinds of data in the elements that are referred to. Note that if you want to specify the length of a null-terminated buffer that is not composed of characters, use the _Nullterm_length_(param) annotation from the previous section.
| Annotation | Description |
|---|---|
_String_length_(param) |
param is the number of elements in the string up to but not including a null terminator. This annotation is reserved for string-of-character types. |
strlen(param) |
param is the number of elements in the string up to but not including a null terminator. This annotation is reserved for use on character arrays and resembles the C Runtime function strlen(). |
wcslen(param) |
param is the number of elements in the string up to (but not including) a null terminator. This annotation is reserved for use on wide character arrays and resembles the C Runtime function wcslen(). |