Для кода 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 через Polyspace панель Configuration. Смотрите Конфигурируют Усовершенствованные Опции Polyspace в Simulink.
Программное обеспечение автоматически импортирует целевые размеры слова и порядок байтов (порядок байтов) от настроек аппаратной конфигурации модели Simulink®. Программное обеспечение сопоставляет настройки Device vendor и Device type на Configuration Parameters Simulink> панель Hardware Implementation к настройкам Target processor type на Polyspace панель Configuration.
Программное обеспечение создает типовую цель для верификации.
