Для 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 Анализ сгенерированного кода.
Для кода 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».
Программное обеспечение автоматически импортирует целевые размеры слова и порядок байтов (endianness) из Simulink® моделирования параметров строения оборудования. Параметры настройки карт <reservedrangesplaceholder5> и <reservedrangesplaceholder4> программного обеспечения на Simulink <reservedrangesplaceholder3>> Hardware Implementation застекляют к Target processor type параметрам настройки на панели Polyspace <reservedrangesplaceholder0>.
Программное обеспечение создает типовой целевой объект для верификации.