Опции 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

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

Можно задать другие опции верификации для Проекта Polyspace через Polyspace панель Configuration. Смотрите Конфигурируют Усовершенствованные Опции Polyspace в Simulink.

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

Программное обеспечение автоматически импортирует целевые размеры слова и порядок байтов (порядок байтов) от настроек аппаратной конфигурации модели Simulink®. Программное обеспечение сопоставляет настройки Device vendor и Device type на Configuration Parameters Simulink> панель Hardware Implementation к настройкам Target processor type на Polyspace панель Configuration.

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