주석 적용 시기 및 위치 지정

  • 아티클

주석이 조건부인 경우 분석기에서 주석을 지정하기 위해 다른 주석이 필요할 수 있습니다. 예를 들어 함수에 동기 또는 비동기 변수가 있는 경우 함수는 다음과 같이 동작합니다. 동기의 경우 항상 성공하지만 비동기에서는 즉시 성공할 수 없는 경우 오류를 보고합니다. 함수가 동기적으로 호출되면 결과 값을 검사 반환되지 않았기 때문에 코드 분석기에 값을 제공하지 않습니다. 그러나 함수가 비동기적으로 호출되고 함수 결과가 검사 않으면 심각한 오류가 발생할 수 있습니다. 이 예제에서는 이 문서의 뒷부분에서 설명한 주석을 사용하여 _When_ 검사 사용할 수 있는 상황을 보여 줍니다.

구조적 주석

주석이 적용되는 시기와 위치를 제어하려면 다음 구조적 주석을 사용합니다.

주석 설명
_At_(expr, anno-list) expr 는 lvalue를 생성하는 식입니다. 주석은 이름이 anno-list 지정된 개체에 적용됩니다 expr. 각 주석의 anno-listexpr 경우 주석이 사전 조건에서 해석되는 경우 사전 조건 및 사후 조건에서 주석이 해석되는 경우 사후 조건에서 해석됩니다.
_At_buffer_(expr, iter, elem-count, anno-list) expr 는 lvalue를 생성하는 식입니다. 주석은 이름이 anno-list 지정된 개체에 적용됩니다 expr. 각 주석의 anno-listexpr 경우 주석이 사전 조건에서 해석되는 경우 사전 조건과 사후 조건에서 주석이 해석되는 경우 사후 조건에서 해석됩니다.

iter 는 주석(포함)으로 범위가 지정된 변수의 anno-list이름입니다. iter 에는 암시적 형식이 있습니다 long. 모든 묶는 범위에서 동일한 이름의 변수는 평가에서 숨겨집니다.

elem-count 는 정수로 계산되는 식입니다.
_Group_(anno-list) 주석 anno-list 은 모두 각 주석에 적용되는 그룹 주석에 적용되는 한정자를 갖는 것으로 간주됩니다.
_When_(expr, anno-list) expr 는 .로 변환 bool할 수 있는 식입니다. 0이 아닌 경우 지정된true 주석 anno-list 이 적용 가능한 것으로 간주됩니다.

기본적으로 각 주석에 anno-listexpr 대해 주석이 사전 조건인 경우 입력 값을 사용하고 주석이 사후 조건인 경우 출력 값을 사용하는 것으로 해석됩니다. 기본값을 재정의하려면 사후 조건을 평가할 때 내장 함수를 사용하여 _Old_ 입력 값을 사용해야 함을 나타낼 수 있습니다. 참고: 변경 가능한 값(예*pLength: 사전 조건의 평가된 결과가 사후 조건의 평가된 결과 expr 와 다를 수 있음)이 관련된 경우 사용 _When_ 결과로 다른 주석을 사용할 수 있습니다.

참고 항목