Версия Windows® Polyspace® Code Prover™ поддерживается для версий 3.5 и 4.0 dSPACE® Словаря Данных и Генератора кода TargetLink®.
Polyspace Code Prover действительно поддерживает сгенерированный код технического директора. Однако для лучших результатов, MathWorks® рекомендует, чтобы вы отключили опцию технического директора в 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.. макс. информация в словаре данных. Эта информация позволяет программному обеспечению Polyspace моделировать действительные значения для системы во время анализа. Тщательно определение информации о минимаксе в модели позволяет анализу быть более точным, потому что только область значений действительных значений анализируется.
Булевы типы моделируются, имея минимальное значение 0 и максимум 1.
Можно также вручную задать ограничительный файл в пользовательском интерфейсе Polyspace. Смотрите Задают Внешние Ограничения. Если вы задаете ограничительный файл, программное обеспечение добавляет автоматически сгенерированную информацию к ограничительному файлу, который вы создаете. Вручную заданная информация об ограничении заменяет автоматически сгенерированную информацию для всех переменных.
Ограничения не могут быть применены к статическим переменным. Поэтому флаги компиляции -D static= установлены автоматически. Это имеет эффект удаления статического ключевого слова из кода. Если вы имеете проблему со столкновениями имени в глобальном пространстве имен, или переименовываете переменные или отключаете эту опцию в настройке Polyspace.
От TargetLink Основное Диалоговое окно этому рекомендуют:
Установите опцию Clean code
Сбросьте опцию Enable sections/pragmas/inline/ISR/user attributes
Выключите генерацию вычислить, чтобы переполниться (CTO). Polyspace может анализировать код, сгенерированный с техническим директором, но результаты не могут быть столь же точными.
Когда вы устанавливаете Polyspace, переменная tlcgOptions обновляется с 'PolyspaceSupport', 'on' (см. переменную в файле 'C:\dSPACE\Matlab\Tl\config\codegen\tl_pre_codegen_hook.m').
