내장 함수
식에 SAL이 부작용 없는 식 하는 C/c + + 식 수-예를 들어, + +,--, 및 모두 부작용이이 컨텍스트에서 함수 호출 합니다.그러나 SAL 함수와 비슷한 오브젝트와 SAL 식에 사용할 수 있는 몇 가지 예약 된 기호를 제공 하지.이를 이라고 내장 함수.
일반 용도
다음과 같은 내장 getarg 함수 주석을 SAL에 대 한 일반 유틸리티를 제공합니다.
주석 |
설명 |
|---|---|
_Curr_ |
현재 주석이 추가 되는 개체에 대 한 동의어입니다.경우는 _At_ 주석 사용 중입니다 _Curr_ 같은 첫 번째 매개 변수를 _At_.그렇지 않으면 주석 어휘 적으로 연관 된 전체 기능/반환 값 또는 매개 변수입니다. |
_Inexpressible_(expr) |
버퍼의 크기는 너무 복잡해 서 주석 식을 사용 하 여 나타낼 수 있는 상황을 표현-예를 들어, 입력된 데이터 집합을 검색 하 고 다음 카운트 계산 됩니다 때 구성원을 선택 합니다. |
_Nullterm_length_(param) |
paramnull 종결자를 포함 하 여 최대 버퍼의 요소 수가입니다.모든 비 집계, void가 아닌 형식의 버퍼에 적용할 수도 있습니다. |
_Old_(expr) |
사전에 계산 하는 경우 _Old_ 입력된 된 값을 반환 합니다. expr.Post-condition에서 계산 되는 경우 값을 반환 expr 이 사전에 확인 된 것 처럼. |
_Param_(n) |
nTh 매개 변수 1에서 계산 하는 함수를 n, 및 n 리터럴 정수 계열 상수입니다.매개 변수가 지정 되 면이 주석 매개 변수 이름으로 액세스를 동일 합니다. .gif "참고") 참고
n에 줄임표에서 정의 하거나 이름이 사용 되지 않는 함수 프로토타입을에 사용 될 수 있습니다 위치 매개 변수를 참조할 수 있습니다.
|
return |
C/c + + 키워드 예약 return SAL 식에서 함수의 반환 값을 나타내는 데 사용할 수 있습니다.게시 상태 값만 사용할 수 있습니다. 그 이전 상태를 사용 하는 구문 오류입니다. |
특정 문자열
다음 내장 함수 주석 문자열을 조작할을 수 있습니다.이러한 함수의 네 모두 같은 용도로 사용: 하기 전에 null 종결자를 찾을 형식의 요소 수를 반환 합니다.차이점의 요소를 참조 하는 데이터의 종류입니다.참고 null로 끝나는 길이 지정 하려는 경우에 버퍼의 문자 구성 됩니다지 않습니다, 사용 하는 _Nullterm_length_(param) 앞 절에서 주석.
주석 |
설명 |
|---|---|
_String_length_(param) |
paramnull 종결자를 포함 하 여 최대 문자열의 요소 수가입니다.이 주석 문자 문자열 형식에 대 한 예약 되어 있습니다. |
strlen(param) |
paramnull 종결자를 포함 하 여 최대 문자열의 요소 수가입니다.이 주석을 사용할 때 문자 배열과 유사한 C 런타임 함수에 대 한 예약 strlen(). |
wcslen(param) |
param요소 문자열 설정 합니다 (제외)의 수는 null 종결자가 있습니다.이 주석을 사용할 때 와이드 문자 배열과 유사한 C 런타임 함수에 대 한 예약 wcslen(). |