Документация

Проверки Polyspace

С программным обеспечением Polyspace Code Prover можно применить верификацию Polyspace к сгенерированному коду Embedded Coder. Программное обеспечение обнаруживает ошибки времени выполнения в сгенерированном коде и помогает вам определить местоположение и зафиксировать отказы модели. Polyspace может подсветить переполнение для определенных операций, которые законны из-за способа, которым генератор кода реализует эти операции. Это законное переполнение не должно быть отмечено Polyspace. Сгенерируйте комментарии в коде, которые подавляют это выявление ошибок.

Генерация кода

1. Откройте модель Simulink в качестве примера mSatAddSub.

model='mSatAddSub';
open_system(model);

2. В приложении Embedded Coder на диалоговое окно Configuration Parameters, выключите аннотации Оператора.

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

3. Чтобы создать модель и сгенерировать код, нажмите Ctrl+B.

evalc('rtwbuild(''mSatAddSub'')');

%The generated code is:
file = fullfile('mSatAddSub_ert_rtw','mSatAddSub.c');
rtwdemodbtype(file,'/* Model step function */',...
    'End of Sum',1,1);

/* 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;
  }

  USub = qY;

4. Осуществите проверку Polyspace. Генератор кода распознает, что самый большой встроенный тип данных является 32-битным. Не возможно насыщать все результаты вычитаний с помощью 0U и больший целочисленный тип данных однословный. Вместо этого программное обеспечение обнаруживает переполнение результатов и направление переполнения, и насыщает результат. Операция отмечается Polyspace, потому что этому не удается распознать насыщение.

5. В приложении Embedded Coder на диалоговое окно Configuration Parameters, выключите аннотации Оператора.

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

6. Сгенерированный код:

file = fullfile('mSatAddSub_ert_rtw','mSatAddSub.c');
rtwdemodbtype(file,'/* Model step function */',...
    'End of Sum',1,1);

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

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

  USub = qY;

Генератор кода вставляет /*MW:OvSatOk*/ прокомментируйте, что это подавляет ошибку, обнаруженную Polyspace.

7. Закройте модель.

bdclose(model)
rtwdemoclean;