Exponenta Banner

полипробел. Класс CodeProverOptions

Пакет: полипробел

Создайте объект Polyspace Code Prover для рукописного кода

расширьте все на странице

Этот класс удерживается от использования и будет удален в будущем релизе. Используйте polyspace.Options вместо этого.

Описание

Настройте верификацию Polyspace® Code Prover™ из MATLAB путем создания объекта опций Программы автоматического доказательства Кода. Чтобы задать исходные файлы и настроить аналитические опции, измените свойства объектов.

Если вы проверяете образцовый сгенерированный код, используйте polyspace.ModelLinkCodeProverOptions вместо этого.

Примечание

Прежде чем вы запустите Polyspace от MATLAB®, необходимо соединить Polyspace и установки MATLAB. Смотрите Интегрируют Polyspace с MATLAB и Simulink.

Конструкция

opts = polyspace.CodeProverOptions создает объект опций Программы автоматического доказательства Кода с опциями для верификации кода С.

opts = polyspace.CodeProverOptions(lang) создает объект опций Программы автоматического доказательства Кода с опциями, применимыми для языка lang.

Входные параметры

развернуть все

Язык верификации задан или как 'C' или как 'CPP'. Этот аргумент определяет, какие свойства объект имеет.

Свойства

Свойства объектов совпадают с аналитическими опциями, найденными в интерфейсе Polyspace. Для получения дополнительной информации синтаксиса смотрите полипробел. Проект. Свойства настройки.

Методы

copyToСкопируйте общие настройки между объектами опций Polyspace
generateProjectСгенерируйте psprj проект от объекта опций
toScriptДобавьте определение объекта опций Polyspace в скрипт

Примеры

свернуть все

Создайте Программу автоматического доказательства Кода, опции возражают и настраивают свойства. Затем запустите верификацию.

Создайте объект и настройте свойства.

sources = fullfile(polyspaceroot, 'polyspace','examples','cxx','Code_Prover_Example', ...
'sources','single_file_analysis.c');
includes = fullfile(polyspaceroot, 'polyspace','examples','cxx','Code_Prover_Example', ...
'sources');
optsCP = polyspace.CodeProverOptions();
optsCP.Prog = 'MyProject';
optsCP.Sources = {sources};
optsCP.EnvironmentSettings.IncludeFolders = {includes};
optsCP.TargetCompiler.Compiler = 'gnu4.7';
optsCP.ResultsDir = tempname;

Запустите анализ и откройте результаты в интерфейсе Polyspace.

results = polyspaceCodeProver(optsCP);
polyspaceCodeProver('-results-dir',optsCP.ResultsDir);

Создайте анализ Программы автоматического доказательства Кода, опции возражают и настраивают свойства. Затем запустите анализ.

Создайте объект и настройте свойства.

sources = fullfile(polyspaceroot, 'polyspace','examples','cxx','Code_Prover_Example', ...
'sources','single_file_analysis.c');
includes = fullfile(polyspaceroot, 'polyspace','examples','cxx','Code_Prover_Example', ...
'sources');
optsCP = polyspace.CodeProverOptions();
optsCP.Prog = 'MyProject';
optsCP.Sources = {sources};
optsCP.EnvironmentSettings.IncludeFolders = {includes};
optsCP.TargetCompiler.Compiler = 'gnu4.7';
optsCP.ResultsDir = tempname;

Сгенерируйте проект Polyspace, назовите его с помощью свойства Prog и откройте проект в интерфейсе Polyspace.

psprj = generateProject(optsCP, optsCP.Prog);
polyspaceCodeProver(psprj);

Можно также анализировать проект из командной строки. Запустите анализ и откройте результаты в интерфейсе Polyspace. 

results = polyspaceCodeProver(psprj, '-nodesktop');
polyspaceCodeProver('-results-dir',optsCP.ResultsDir);

Альтернативы

Если вы проверяете образцовый сгенерированный код, используйте polyspace.ModelLinkCodeProverOptions вместо этого.

Смотрите также

| |

Темы

Введенный в R2017b

Документация Polyspace Code Prover
Поддержка