Опции Polyspace по умолчанию для кода, сгенерированного Embedded Coder

Опции по умолчанию

Для Embedded Coder® код, программное обеспечение по умолчанию устанавливает следующие опции верификации:

-sources path_to_source_code
-D PST_ERRNO
-D main=main_rtwec
-I matlabroot\polyspace\include
-I matlabroot\extern\include
-I matlabroot\rtw\c\libsrc
-I matlabroot\simulink\include 
-I matlabroot\sys\lcc\include
-functions-to-stub=[rtIsNaN,rtIsInf,rtIsNaNF,rtIsInfF]
-results-dir results

Примечание

matlabroot является MATLAB® папка установки.

Спецификация ограничений

Можно ограничивать входы, параметры и выходы так, чтобы они лежали в заданных областях. Используйте следующие параметры конфигурации:

Программа автоматически создает Polyspace® файл ограничений с использованием информации из рабочей области MATLAB и параметров блоков.

Можно также вручную задать файл ограничений в пользовательском интерфейсе Polyspace. См. «Задание внешних ограничений». Если вы задаете файл ограничений, программное обеспечение добавляет автоматически сгенерированную информацию к файлу ограничений, который вы создаете. Вручную заданная информация о ограничениях переопределяет автоматически сгенерированную информацию для всех переменных.

Программное обеспечение поддерживает автоматическую генерацию спецификаций ограничений для следующих видов сгенерированного кода:

  • Код из автономных моделей

  • Код из сконфигурированных прототипов функций

  • Переиспользуемый код

  • Код, сгенерированный из ссылочных моделей и подмоделей

Дополнительная информация

Смотрите также Внешние ограничения на Polyspace Анализ сгенерированного кода.

Рекомендуемые опции Polyspace для проверки сгенерированного кода

Для кода Embedded Coder программное обеспечение автоматически задает значения для следующих опций верификации:

  • -main-generator

  • -functions-called-in-loop

  • -functions-called-before-loop

  • -functions-called-after-loop

  • -variables-written-in-loop

  • -variables-written-before-loop

Embedded Coder выполняет обтекание переменных в сгенерированном коде, которое может переполниться. При запуске анализа кода, сгенерированного Embedded Coder, Polyspace использует следующие опции:

  • -signed-integer-overflows warn-with-wrap-around

  • -unsigned-integer-overflows allow

Эти опции могут иметь различные значения по умолчанию при анализе кода, который не генерируется Embedded Coder. См. Overflow mode for signed integer (-signed-integer-overflows) и Overflow mode for unsigned integer (-unsigned-integer-overflows).

В сложение для опции -serverпрограмма использует значение, заданное в флажке Send to Polyspace server на панели Polyspace. Эти значения переопределяют соответствующие значения опций на панели Configuration пользовательского интерфейса Polyspace.

Можно задать другие опции верификации для проекта Polyspace с помощью панели Configuration Polyspace. См. раздел «Настройка дополнительных опций Polyspace в Simulink».

Аппаратное отображение между Simulink и Polyspace

Программное обеспечение автоматически импортирует целевые размеры слова и порядок байтов (endianness) из Simulink® моделирования параметров строения оборудования. Параметры настройки карт <reservedrangesplaceholder5> и <reservedrangesplaceholder4> программного обеспечения на Simulink <reservedrangesplaceholder3>> Hardware Implementation застекляют к Target processor type параметрам настройки на панели Polyspace <reservedrangesplaceholder0>.

Программное обеспечение создает типовой целевой объект для верификации.