내장 함수
SAL의 식은 부작용이 없는 식인 경우 C/C++ 식일 수 있습니다. 예를 들어 ++, --, 및 함수 호출은 모두 이 컨텍스트에서 부작용이 있습니다. 그러나 SAL은 함수와 유사한 몇몇 개체와 SAL 식에 사용할 수 있는 몇몇 예약된 기호를 제공합니다. 이를 내장 함수라고 합니다.
범용
다음 내장 함수 주석은 SAL에 대한 일반적인 유틸리티를 제공합니다.
| 주석 | 설명 |
|---|---|
_Curr_ |
현재 주석이 달리고 있는 개체의 동의어입니다. _At_ 주석이 사용되는 경우 _Curr_는 _At_의 첫 번째 매개 변수와 동일합니다. 그렇지 않으면 주석이 어휘적으로 연관된 매개 변수 또는 전체 함수/반환 값입니다. |
_Inexpressible_(expr) |
버퍼의 크기가 너무 복잡하여 주석 식을 사용하여 표현할 수 없는 상황을 표현합니다. 예를 들어 입력 데이터 세트를 스캔한 다음 선택한 멤버를 세어 계산하는 경우입니다. |
_Nullterm_length_(param) |
param은 버퍼 내 null 종결자 앞까지의 요소 수입니다. 비 집계, 비 void 형식의 버퍼에 적용할 수 있습니다. |
_Old_(expr) |
사전 조건에서 평가되면 _Old_는 입력 값 expr을 반환합니다. 사후 조건에서 평가되면 사전 조건에서 평가되었을 때처럼 값 expr을 반환합니다. |
_Param_(n) |
1에서 n까지 계산되는 함수의 n 번째 매개 변수로, n은 리터럴 적분 상수입니다. 매개 변수 이름이 지정되면 이 주석은 이름으로 매개 변수에 액세스하는 것과 동일합니다. 참고: n은 줄임표로 정의되는 위치 매개 변수를 참조하거나 이름이 사용되지 않는 함수 프로토타입에 사용될 수 있습니다. |
return |
C/C++ 예약 키워드 return을 SAL 식에서 함수의 반환 값을 나타내는 데 사용할 수 있습니다. 이 값은 사후 상태에서만 사용할 수 있으며, 사전 상태에서 사용하는 것은 구문 오류입니다. |
특정 문자열
다음 내장 함수 주석을 사용하면 문자열을 조작할 수 있습니다. 이러한 네 가지 함수는 모두 null 종결자 앞에 있는 형식의 요소 수를 반환하는 동일한 용도로 사용됩니다. 다른 점은 참조하는 요소의 데이터 종류입니다. 문자로 구성되지 않는 null로 끝나는 버퍼의 길이를 지정하려면 이전 섹션의 _Nullterm_length_(param) 주석을 사용합니다.
| 주석 | 설명 |
|---|---|
_String_length_(param) |
param은 문자열 내 null 종결자 앞까지의 요소 수입니다. 이 주석은 문자열 형식에 사용하도록 예약되어 있습니다. |
strlen(param) |
param은 문자열 내 null 종결자 앞까지의 요소 수입니다. 이 주석은 문자 배열에서 사용하도록 예약되어 있으며, C 런타임 함수 strlen()과 유사합니다. |
wcslen(param) |
param 문자열 내 null 종결자(포함하지 않음) 앞까지의 요소 수입니다. 이 주석은 와이드 문자 배열에서 사용하도록 예약되어 있으며, C 런타임 함수 wcslen()과 유사합니다. |