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

Поддержка