Main Content

polyspaceCodeProverServer

Run Polyspace Code Prover verification from MATLAB

collapse all in page

For easier scripting, run Polyspace® analysis using a polyspace.Project object.

Syntax

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

Description

polyspaceCodeProverServer(optsObject) runs a verification on the Polyspace options object in MATLAB®.

example

polyspaceCodeProverServer('-help') displays all options that can be supplied to the polyspaceCodeProverServer command to run a Polyspace Code Prover™ verification.

polyspaceCodeProverServer('-sources',sourceFiles) runs a Polyspace Code Prover verification on the source files specified in sourceFiles.

example

polyspaceCodeProverServer('-sources',sourceFiles,Name,Value) runs a Polyspace Code Prover verification on the source files with additional options specified by one or more Name,Value pair arguments.

Note

Before you run Polyspace from MATLAB, you must link your Polyspace and MATLAB installations. See Integrate Polyspace Server Products with MATLAB.

example

Examples

collapse all

This example shows how to run a Polyspace verification from the MATLAB command-line. For this example:

  • Use the source file numerical.c located in the directory polyspaceroot/polyspace/examples/cxx/BugFinder_example/sources.

  • Include the headers located in the same directory.

Create an options object and add the source file and include folder to the properties.

opts = polyspace.Options;
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';

Run the analysis and view the results.

polyspaceCodeProverServer(opts);

A Code Prover analysis runs on the file C:\Polyspace_Sources\source.c and stores the result in C:\Polyspace_Results.

This example shows how to run a Polyspace verification on a single source file by using DOS/UNIX Options. For this example:

  • Use the source file numerical.c located in the directory polyspaceroot/polyspace/examples/cxx/BugFinder_example/sources.

  • Include the headers located in the same directory.

Define the location of source and include files.

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');

Run the verification and open the results.

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

This example shows two different ways to customize a verification in MATLAB. You can customize as many additional options as you want by changing properties in an options object or by using Name-Value pairs. You specify checking of MISRA C™ 2012 coding rules, exclude headers from coding rule checking, and generate a main.

To create variables for source file path, include folder path, and results folder path that you can use for either analysis method.

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');

Verify coding rules with an options object.

opts = polyspace.Options('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);

Verify coding rules with DOS/UNIX options.

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

Input Arguments

collapse all

Polyspace options object name, specified as the object handle.

To create an options object, use one of the Polyspace options classes: polyspace.Options or polyspace.Project.

Example: opts

Comma-separated source file names with extension .c or .cpp, specified as a single character vector.

If the files are not in the current folder, sourceFiles must include a full or relative path.

Example: 'myFile.c', 'C:\mySources\myFile1.c,C:\mySources\myFile2.c'

Name-Value Arguments

Specify optional pairs of arguments as Name1=Value1,...,NameN=ValueN, where Name is the argument name and Value is the corresponding value. Name-value arguments must appear after other arguments, but the order of the pairs does not matter.

Before R2021a, use commas to separate each name and value, and enclose Name in quotes.

Example: '-target','i386','-compiler','gnu4.6' specifies that the source code is intended for i386 processors and contains non-ANSI C syntax for the GCC 4.6 compiler.

For the full list of analysis options, see Complete List of Polyspace Code Prover Analysis Options.

Version History

Introduced in R2019a

See Also

Topics