이 페이지는 기계 번역을 사용하여 번역되었습니다. 영어 원문을 보려면 여기를 클릭하십시오.

Polyspace 검사를 정당화하기 위한 코드 주석 달기

스크립트 열기

이 예제는 Embedded Coder®가 생성된 코드에서 연산자 주석을 사용하여 특정 산술 연산을 정당화하고, 정적 코드 분석 시 Polyspace의 오류 탐지를 억제하는 방법을 보여줍니다.

Polyspace Code Prover™를 사용하면 Embedded Coder로 수행된 코드 생성에 대해 Polyspace 정적 검증을 수행할 수 있습니다. Polyspace는 생성된 코드에서 런타임 오류를 감지하고 모델링상의 결함을 파악하는 데 도움을 줍니다. 경우에 따라 Polyspace는 코드 생성기가 해당 연산을 구현하는 방식 때문에 설계상 안전한 연산에 대해서도 오버플로우를 보고하기도 합니다. 이러한 결과는 오류로 보고되어서는 안 됩니다. Operator annotations를 활성화하면, Embedded Coder는 생성된 코드에 해당 연산의 의도를 설명하는 주석을 삽입합니다. Polyspace는 이러한 주석을 사용하여 해당 분석 결과를 표시하지 않도록 합니다. 이 주석들은 분석 목적으로만 사용되며, 생성된 C 코드의 의미론에는 영향을 미치지 않습니다. 자세한 내용은 Automated Justification of Coding Rule Violations (Polyspace Bug Finder) 항목을 참조하십시오.

포화 오버플로우에 대한 근거

이 섹션에서는 연산자 어노테이션이 코드 생성 과정에서 나타나는 포화 현상을 어떻게 설명하는지 보여줍니다.

1. 예제 모델 mSatAddSub을 엽니다.

model='mSatAddSub';
open_system(model);

2. Embedded Coder 앱에서 구성 파라미터 대화 상자를 열고 연산자 주석을 off로 설정하십시오.

set_param('mSatAddSub','OperatorAnnotations','off');

3. 모델을 구축하고 코드를 생성합니다.

evalc('slbuild(''mSatAddSub'')');

생성된 코드 파일을 확인합니다:

file = fullfile('mSatAddSub_ert_rtw','mSatAddSub.c');
coder.example.extractLines(file,'/* Model step function */',...
    'USub = qY;');

/* Model step function */
void mSatAddSub_step(void)
{
  uint32_T qY;

  /* Sum: '<Root>/SubUnsigned' incorporates:
   *  Inport: '<Root>/In1'
   *  Inport: '<Root>/In2'
   */
  qY = U1 - U2;
  if (qY > U1) {
    qY = 0U;
  }

  /* Sum: '<Root>/SubUnsigned' */

코드 생성기는 U1 및 U2에 대해 가장 큰 내장 정수형(32비트)을 사용하여 뺄셈 연산을 수행합니다. 모든 포화 결과를 직접 표현할 수 없기 때문에, 생성된 코드는 먼저 뺄셈 연산을 수행한 다음 오버플로를 감지하고, 마지막으로 명시적인 포화 로직을 적용합니다. Polyspace는 설계상 최종 동작이 안전함에도 불구하고, 포화 논리를 추론하지 않기 때문에 해당 뺄셈 연산을 산술 오버플로로 표시할 수 있습니다.

5. 구성 파라미터 대화 상자에서 연산자 주석을 활성화한 다음 모델을 빌드합니다.

set_param('mSatAddSub','OperatorAnnotations',"on");
evalc('slbuild(''mSatAddSub'')');

6. 생성된 코드를 살펴봅니다:

file = fullfile('mSatAddSub_ert_rtw','mSatAddSub.c');
coder.example.extractLines(file,'/* Model step function */',...
    'USub = qY;');

/* Model step function */
void mSatAddSub_step(void)
{
  uint32_T qY;

  /* Sum: '<Root>/SubUnsigned' incorporates:
   *  Inport: '<Root>/In1'
   *  Inport: '<Root>/In2'
   */
  qY = U1 -
    /*MW:operator MISRA2012:D4.1 CERT-C:INT30-C 'Justifying MISRA C rule violation'*/
    /*MW:OvSatOk*/ U2;
  if (qY > U1) {
    qY = 0U;
  }

  /* Sum: '<Root>/SubUnsigned' */

연산자 주석 파라미터가 활성화되면 Embedded Coder는 /*MW:OvSatOk*/ 주석을 삽입합니다. 이 어노테이션은 산술 오버플로가 의도된 것임을 나타내며, Polyspace는 이 주석(annotation)을 사용하여 코드 분석 시 오버플로 오류를 억제합니다.

7. 모델을 닫으십시오.

bdclose(model)

캐리 또는 차입 감지 논증 (MW:OvCarryOk)

경우에 따라 생성된 코드는 자리 넘침(carry) 또는 자리 빌림(borrow) 조건을 감지하기 위해 의도적으로 부호 없는 정수의 래핑(wraparound) 동작을 이용하기도 합니다. Polyspace는 감싸기 현상이 의도된 것임을 인식하지 못하기 때문에, 이러한 연산을 산술 오버플로로 표시할 수 있습니다.

연산자 주석이 활성화된 상태에서, Embedded Coder는 해당 연산이 의도된 것임을 나타내기 위해 MW:OvCarryOk 주석을 삽입합니다.

uint32_T qY;
boolean_T borrow;

qY = U1 - /*MW:OvCarryOk*/ U2;
borrow = (qY > U1);

MW:OvCarryOk 주석은 오버플로 동작이 의도된 것이며, 이월 또는 차입 조건을 감지하는 데 사용됨을 나타냅니다. Polyspace는 해당 오버플로 분석 결과를 표시하지 않습니다.

비트 단위 절삭의 타당성 (MW:OvBitwiseOk)

드문 경우지만, 생성된 코드는 마스킹과 같은 비트 단위 연산을 통해 고차 비트를 의도적으로 제거하기도 합니다. Polyspace는 절단이 의도된 것임을 인식하지 못하기 때문에 해당 산술 연산을 오버플로우로 표시할 수 있습니다.

연산자 어노테이션이 활성화된 상태에서, Embedded Coder는 이러한 동작을 나타내기 위해 MW:OvBitwiseOk 어노테이션을 삽입합니다.

uint32_T qY;

qY = (U1 + /*MW:OvBitwiseOk*/ U2) & 0xFFU;

MW:OvBitwiseOk 주석은 해당 연산으로 인해 발생하는 오버플로우나 비트 손실이 후속 비트 단위 처리 과정에 따라 의도된 것임을 나타냅니다. Polyspace는 해당 분석 결과를 표시하지 않습니다.

참고 항목

도움말 항목