Кодирование правила и параметров конфигурации для кода С, заданного как:

Пример: opt.VerificationSettings = 'PrjConfigAndMisraC2012'

Режим Polyspace^®, заданный как 'BugFinder', для анализа Bug Finder или 'CodeProver', для верификации Программы автоматического доказательства Кода.

Пример: opt.VerificationMode = 'BugFinder';

Позволяет файл пользовательской конфигурации вместо настройки по умолчанию, заданной как TRUE или FALSE. Используйте PrjConfigFile опция, чтобы задать конфигурационный файл.

Пример: opt.EnablePrjConfigFile = true;

Файл пользовательской конфигурации, чтобы использовать вместо настройки по умолчанию, заданной полным путем к .psprj файл. Используйте EnablePrjConfigFile опция, чтобы использовать этот конфигурационный файл во время вашего анализа.

Пример: opt.PrjConfigFile = 'C:\Polyspace\config.psprj';

Это наборы свойств уровень проверки настройки, сделанной перед анализом, запускается. Проверка настройки перед анализом задана как:

Пример: opt.CheckConfigBeforeAnalysis = 'OnHalt';

Имя папки результатов и местоположение, заданное как локальное имя папки или путь к папке. Эта папка - то, где Polyspace пишет результаты анализа. Это имя папки может быть или абсолютным путем или путем относительно текущей папки. Текст $ModelName$ заменяется именем исходной модели.

Пример: opt.ResultDir = '\results_v1_$ModelName$';

Добавьте уникальный номер в имя папки результатов, заданное как TRUE или FALSE. Если это правда, уникальный номер добавляется в конец каждого нового результата. Используя эту опцию помогает вам постараться не перезаписывать предыдущие папки результатов.

Пример: opt.AddSuffixToResultDir = true;

Откройте среду Polyspace, чтобы контролировать прогресс анализа в виде TRUE или FALSE. Позже, можно рассмотреть результаты.

Пример: opt.OpenProjectManager = true;

Добавьте свои результаты в в настоящее время открытый проект Simulink, если таковые имеются, заданный как TRUE или FALSE. Эта опция позволяет вам сохранять свои результаты Polyspace организованными с остальной частью ваших файлов проекта. Если проект Simulink не открыт, результаты не добавляются к проекту Simulink.

Пример: opt.AddToSimulinkProject = true;

Позвольте дополнительному списку файлов анализироваться в виде TRUE или FALSE. Используйте с AdditionalFileList опция.

Пример: opt.EnableAdditionalFileList = true;

Список дополнительных файлов, которые будут анализироваться заданный как массив ячеек файлов. Используйте с EnableAdditionalFileList опция, чтобы добавить эти файлы в анализ.

Пример: opt.AdditionalFileList = {'sources\file1.c', 'sources\file2.c'};

Типы данных: cell

Включите информацию области значений проекта, указанную как 'DesignMinMax', использовать области значений данных, заданные в блоках и рабочих областях или 'FullRange', обрабатывать входные параметры как полнофункциональные значения.

Пример: opt.InputRangeMode = 'FullRange';

Включите постоянные значения параметров в виде 'None', использовать постоянные значения параметров, заданные в коде или 'DesignMinMax' использовать область значений, заданную в блоках и рабочих областях.

Пример: opt.ParamRangeMode = 'DesignMinMax';

Включите выходные утверждения, заданные 'None', не применять утверждения или 'DesignMinMax' применять утверждения к выходным параметрам с помощью области значений, заданной в блоках и рабочей области.

Пример: opt.ParamRangeMode = 'DesignMinMax';

Задайте глубину для анализа моделей, на которые ссылается текущая модель.

Для Embedded Coder^® только

Пример: opt.ModelRefVerifDepth = '3';

Задайте, хотите ли вы анализировать все модели, на которые ссылаются, вместе или анализировать модели индивидуально.

Для Embedded Coder только

Пример: opt.ModelRefByModelRefVerif = true;

Кодирование правила и параметров конфигурации для Кода С++, заданного как:

Только для Embedded Coder

Пример: opt.CxxVerificationSettings = 'MisraCxx';

Использование Интерполяционной таблицы кода в виде TRUE или FALSE.

Только для TargetLink^®

Пример: opts.AutoStubLUT = true;