Exponenta Banner

polyspaceCodeProverServer

Запустите верификацию Polyspace Code Prover из MATLAB

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

Для более легких сценариев запустите Polyspace® анализ с помощью polyspace.Project объект.

Синтаксис

polyspaceCodeProverServer(optsObject)
polyspaceCodeProverServer('-help')
polyspaceCodeProverServer('-sources',sourceFiles)
polyspaceCodeProverServer('-sources',sourceFiles,Name,Value)

Описание

пример

polyspaceCodeProverServer(optsObject) запускает верификацию на объекте опций Polyspace в MATLAB®.

polyspaceCodeProverServer('-help') отображения все опции, которые могут быть предоставлены polyspaceCodeProverServer команда, чтобы запустить верификацию Polyspace Code Prover™.

пример

polyspaceCodeProverServer('-sources',sourceFiles) запускает верификацию Polyspace Code Prover на исходных файлах, заданных в sourceFiles.

пример

polyspaceCodeProverServer('-sources',sourceFiles,Name,Value) запускает верификацию Polyspace Code Prover на исходных файлах с дополнительными опциями, заданными одним или несколькими Name,Value парные аргументы.

Примечание

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

Примеры

свернуть все

В этом примере показано, как запустить верификацию Polyspace из командной строки MATLAB. Для этого примера:

  • Используйте исходный файл numerical.c расположенный в директории polyspaceroot/polyspace/examples/cxx/BugFinder_example/sources.

  • Включайте заголовки, расположенные в ту же директорию.

Создайте, опции возражают и добавляют исходный файл и включают папку в свойства.

opts = polyspace.CodeProverOptions;
opts.Sources = {fullfile(polyspaceroot, 'polyspace', 'examples',...
    'cxx', 'Bug_Finder_Example', 'sources', 'numerical.c')};;
opts.EnvironmentSettings.IncludeFolders = {fullfile(polyspaceroot, 'polyspace', 'examples',...
    'cxx', 'Bug_Finder_Example', 'sources')};
opts.ResultsDir = 'C:\Polyspace_Results';

Запустите верификацию и просмотрите результаты.

polyspaceCodeProverServer(opts);

Polyspace работает на файле C:\Polyspace_Sources\source.c и хранит результат в C:\Polyspace_Results.

В этом примере показано, как запустить верификацию Polyspace на одном исходном файле при помощи Опций DOS/UNIX. Для этого примера:

  • Используйте исходный файл numerical.c расположенный в директории polyspaceroot/polyspace/examples/cxx/BugFinder_example/sources.

  • Включайте заголовки, расположенные в ту же директорию.

Задайте местоположение источника и включайте файлы.

src = fullfile(polyspaceroot, 'polyspace', 'examples',...
    'cxx', 'Bug_Finder_Example', 'sources', 'numerical.c');
inc = fullfile(polyspaceroot, 'polyspace', 'examples',...
    'cxx', 'Bug_Finder_Example', 'sources');
res = fullfile(pwd,'results');

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

polyspaceCodeProverServer('-sources',src, ...
    '-I',inc, ...
    '-results-dir',res)

Этот пример показывает два различных способа настроить верификацию в MATLAB. Можно настроить столько дополнительных опций, сколько вы хотите путем изменения свойств в объекте опций или при помощи Пар "имя-значение". Вы задаете проверку MISRA C® 2 012 правил кодирования, исключите заголовки из кодирования проверки правила и сгенерируйте основное.

Чтобы создать переменные для пути к исходному файлу, включайте путь к папке, и заканчивается путь к папке, который можно использовать для любого метода анализа.

sourceFileName = fullfile(polyspaceroot, 'polyspace','examples', 'cxx', 'Code_Prover_Example','sources','example.c');
includeFileName = fullfile(polyspaceroot, 'polyspace','examples', 'cxx', 'Code_Prover_Example','sources','include.h');
resFolder1 = fullfile('Polyspace_Results_1');
resFolder2 = fullfile('Polyspace_Results_2');

Проверьте правила кодирования с объектом опций.

opts = polyspace.CodeProverOptions('C');
opts.Sources = {sourceFileName};
opts.EnvironmentSettings.IncludeFolders = {includeFileName};
opts.ResultsDir = resFolder1;
opts.CodingRulesCodeMetrics.EnableMisraC3 = true;
opts.CodingRulesCodeMetrics.MisraC3Subset = 'mandatory';
opts.CodeProverVerification.EnableMain = true;
opts.InputsStubbing.DoNotGenerateResultsFor = 'all-headers';
polyspaceCodeProverServer(opts);

Проверьте правила кодирования с опциями DOS/UNIX.

polyspaceCodeProverServer('-sources',sourceFileName,...
     '-I',includeFileName, ...
     '-results-dir',resFolder2,...
     '-misra3','mandatory',...
     '-do-not-generate-results-for','all-headers',...
     '-main-generator');

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

свернуть все

Имя объекта опций Polyspace в виде указателя на объект.

Чтобы создать объект опций, используйте один из классов опций Polyspace: polyspace.Options или polyspace.Project.

Пример: opts

Разделенный от запятой исходный файл называет с дополнительным .c или .cppВ виде односимвольного вектора.

Если файлы не находятся в текущей папке, sourceFiles должен включать полный или относительный путь.

Пример: 'myFile.c', 'C:\mySources\myFile1.c,C:\mySources\myFile2.c'

Аргументы name-value

Задайте дополнительные разделенные запятой пары Name,Value аргументы. Name имя аргумента и Value соответствующее значение. Name должен появиться в кавычках. Вы можете задать несколько аргументов в виде пар имен и значений в любом порядке, например: Name1, Value1, ..., NameN, ValueN.

Пример: '-target','i386','-compiler','gnu4.6' указывает, что исходный код предназначается для i386 процессоров и содержит Синтаксис C не-ANSI для компилятора GCC 4.6.

Для полного списка опций анализа см. Полный список Опций анализа Polyspace Code Prover.

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

Темы

Введенный в R2019a

Документация Polyspace Code Prover

Поддержка