주석 적용 시기 및 위치 지정
조건부 주석의 경우 분석기를 지정 하는 다른 주석 필요 합니다.함수에는 동기 또는 비동기일 수 있습니다 변수 있으면 예를 들어,는 함수는 다음과 같이 동작 합니다: 동기 i/o의 경우에는 항상 결국 성공 하지만 비동기 바로 성공할 수 없는 경우 오류를 보고 합니다.함수는 동기적으로 호출 되 면 결과 값 검사 값이 없는 코드 분석기 반환 된 것 때문에 제공 합니다.그러나 비동기적으로 호출 되는 함수 및 함수 결과 선택 하지 않은 경우 심각한 오류가 발생할 수 있습니다.사용할 수 있는 상황을 보여 주는이 예제는 _When_ 주석-이 문서의 뒷부분에 설명 된-검사를 사용 하려면.
구조적 주석
시기 및 위치에 주석 적용을 제어 하려면 다음 구조 주석을 사용 합니다.
주석 |
설명 |
|---|---|
_At_(expr, anno-list) |
exprlvalue를 산출 하는 식이입니다.주석에서 anno-list 에서 명명 된 개체에 적용 된 expr.각 주석에서 anno-list, expr 사전에 주석 사전에서 해석 되 고 post-condition에서 post-condition 있는 경우 주석을 해석 해석 됩니다. |
_At_buffer_(expr, iter, elem-count, anno-list) |
exprlvalue를 산출 하는 식이입니다.주석에서 anno-list 에서 명명 된 개체에 적용 된 expr.각 주석에서 anno-list, expr 사전에 주석 사전에서 해석 되 고 post-condition에서 post-condition 있는 경우 주석을 해석 해석 됩니다. iter주석으로 범위가 지정 되는 변수의 이름입니다 (포함 anno-list).iter암시적 형식이 long.같은 이름의 변수를 포함 하는 범위에서 평가 숨겨져 있습니다. elem-count정수 값을 계산 하는 식이입니다. |
_Group_(anno-list) |
주석에서 anno-list 모든 각 주석에 적용 되는 그룹 주석에 적용 되는 한정자가 간주 됩니다. |
_When_(expr, anno-list) |
expr변환할 수 있는 식은 bool.0이 아닌 경우 (true)에 지정 된 주석 anno-list 적용 가능한 것으로 간주 됩니다. 기본적으로 각 주석에서 anno-list, expr 주석을 전제 조건, 경우 출력 값을 사용으로 주석 post-condition의 경우 입력된 값을 사용 하는 것으로 해석 됩니다.사용 하 여 기본값을 무시는 _Old_ 는 post-condition 입력된 값을 사용 해야 함을 나타내려면 평가할 때 내장. .gif "참고") 참고
다른 주석 수 있습니다 사용 하 여 결과로 _When_ 변경 가능한 값을 사용할 경우-예를 들어, *pLength-있기 때문에 관련 된 평가 결과를 expr 전제 조건에 계산된 결과가 post-condition에서 다를 수 있습니다.
|