Windows® версия Polyspace® Code Prover™ поддерживается для версий 3.5 и 4.0 dSPACE® Словарь данных и TargetLink® Генератор кода.
Polyspace Code Prover поддерживает сгенерированный код CTO. Однако для лучших результатов MathWorks® рекомендует отключить опцию CTO в TargetLink перед генерацией кода. Для получения дополнительной информации см. документацию dSPACE.
Поскольку Polyspace Code Prover извлекает информацию из словаря данных 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= устанавливается автоматически. Он имеет эффект удаления статического ключевого слова из кода. Если у вас есть проблема с конфликтами имен в глобальном пространстве имен, либо переименуйте переменные, либо отключите эту опцию в строении 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' файл).
