exponenta event banner

Параметры Polyspace по умолчанию для кода, созданного с помощью встроенного кодера

Параметры по умолчанию

Для кода 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. См. раздел Указание внешних ограничений. При определении файла ограничений программа добавляет автоматически сгенерированную информацию к создаваемому файлу ограничений. Информация об ограничениях, определенная вручную, переопределяет автоматически сгенерированную информацию для всех переменных.

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

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

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

  • Многократно используемый код

  • Код, генерируемый ссылочными моделями и подмоделями

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

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

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

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

  • -main-generator

  • -functions-called-in-loop

  • -functions-called-before-loop

  • -functions-called-after-loop

  • -variables-written-in-loop

  • -variables-written-before-loop

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

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

  • -unsigned-integer-overflows allow

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

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

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

Аппаратное сопоставление между Simulink и Polyspace

Программное обеспечение автоматически импортирует целевые длины слов и порядок байтов (endianness) из настроек конфигурации оборудования модели Simulink ®. Программа сопоставляет параметры Поставщик устройства и Тип устройства на панели Параметры конфигурации Simulink > Аппаратная реализация с параметрами Тип целевого процессора на панели Конфигурация Polyspace.

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