Exponenta Banner

polyspace.CodeProverOptions class

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

Создайте объект 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. Для получения дополнительной информации синтаксиса смотрите polyspace.Project.Configuration Properties.

Методы

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
Поддержка