Версия Windows ® Polyspace ® Code Prover™ поддерживается для версий 3.5 и 4.0 dSPACE ® Data Dictionary и TargetLink ® Code Generator.
Программа проверки кода Polyspace поддерживает созданный код CTO. Однако для улучшения результатов MathWorks ® рекомендует отключить параметр CTO в TargetLink перед созданием кода. Дополнительные сведения см. в документации dSPACE.
Поскольку средство проверки кода Polyspace извлекает информацию из словаря данных dSPACE, перед выполнением анализа необходимо повторно создать код.
По умолчанию Polyspace задает следующие параметры:
-sources path_to_source_code -results-dir results_folder_name -I path_to_source_code -D PST_ERRNO -I dspaceroot\matlab\TL\SimFiles\Generic -I dspaceroot\matlab\TL\srcfiles\Generic -I dspaceroot\matlab\TL\srcfiles\i86\LCC -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] -scalar-overflows-behavior wrap-around -boolean-types Bool
Примечание
dspaceroot и matlabroot - каталоги установки инструментов dSPACE и MATLAB ® соответственно.
По умолчанию Polyspace предоставляет заглушки для функций таблицы подстановки. Словарь данных dSPACE используется для определения диапазона возвращаемых значений. Таблица подстановки, использующая экстраполяцию, возвращает полный диапазон для типа возвращаемой переменной. Это поведение можно отключить в меню настройки Polyspace.
Можно ограничить входные данные, параметры и выходные данные в пределах заданных диапазонов данных. См. раздел Работа с диапазонами сигналов в блоках (Simulink).
Программа автоматически создает файл ограничений Polyspace с использованием словаря данных dSPACE для каждой глобальной переменной. Информация об ограничении используется для инициализации каждой глобальной переменной в диапазоне допустимых значений, определяемых информацией min.. max в словаре данных. Эта информация позволяет программному обеспечению Polyspace моделировать реальные значения для системы во время анализа. Тщательное определение информации min-max в модели позволяет сделать анализ более точным, поскольку анализируется только диапазон реальных значений.
Примечание
Логические типы моделируются с минимальным значением 0 и максимальным значением 1.
Можно также вручную определить файл ограничений в интерфейсе пользователя Polyspace. См. раздел Указание внешних ограничений. При определении файла ограничений программа добавляет автоматически сгенерированную информацию к создаваемому файлу ограничений. Информация об ограничениях, определенная вручную, переопределяет автоматически сгенерированную информацию для всех переменных.
Нельзя применять ограничения к статическим переменным. Поэтому флаги компиляции -D static= устанавливается автоматически. Это приводит к удалению ключевого слова static из кода. При возникновении проблем с конфликтами имен в глобальном пространстве имен переименуйте переменные или отключите этот параметр в конфигурации Polyspace.
В главном диалоговом окне TargetLink рекомендуется:
Установка опции Clean code
Отмена настройки опции Enable sections/pragmas/inline/ISR/user attributes
Выключите вычисление для генерации переполнения (CTO). Polyspace может анализировать код, сгенерированный с помощью CTO, но результаты могут быть не столь точными.
При установке Polyspace tlcgOptions переменная обновляется с помощью 'PolyspaceSupport', 'on' (см. переменную в 'C:\dSPACE\Matlab\Tl\config\codegen\tl_pre_codegen_hook.m' файл).