polyspaceCodeProver

Run Polyspace Code Prover verification from MATLAB

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

Syntax

polyspaceCodeProver

status = polyspaceCodeProver(projectFile)

status = polyspaceCodeProver(optsObject)

status = polyspaceCodeProver(projectFile, '-nodesktop')

status = polyspaceCodeProver(resultsFile)

status = polyspaceCodeProver('-results-dir',resultsFolder)

status = polyspaceCodeProver('-help')

status = polyspaceCodeProver('-sources',sourceFiles)

polyspaceCodeProver('-sources',sourceFiles,Name,Value)

[status, jobID] = polyspaceCodeProver(___,'-batch','-scheduler',scheduler)

Description

polyspaceCodeProver opens Polyspace Code Prover™.

status = polyspaceCodeProver(projectFile) opens a Polyspace project file in Polyspace Code Prover.

status = polyspaceCodeProver(optsObject) runs a verification on the Polyspace options object in MATLAB^®.

Note

When you use a Polyspace options object to run an analysis, use only the Polyspace options object to specify options of the analysis. Using name-value arguments is not supported when the first argument is a Polyspace options object.

status = polyspaceCodeProver(projectFile, '-nodesktop') runs a verification on the Polyspace project file in MATLAB. If you have multiple modules or configurations, Polyspace runs the active configuration and active module. To see which module and configuration are active, open the project in the Polyspace interface and look for the bold, selected module and configuration. To change which module or configuration is active, before closing the Polyspace interface, select the module and configuration you want to verify.

status = polyspaceCodeProver(resultsFile) opens a Polyspace results file in Polyspace Code Prover.

status = polyspaceCodeProver('-results-dir',resultsFolder) opens a Polyspace results file from resultsFolder in Polyspace Code Prover.

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

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

polyspaceCodeProver('-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 with MATLAB and Simulink.

[status, jobID] = polyspaceCodeProver(___,'-batch','-scheduler',scheduler) offloads the analysis to a remote cluster. Here, scheduler specifies the head node of the cluster that manages the analysis submissions from multiple clients. See also Manipulate Two Jobs in the Cluster.

Examples

Open Polyspace Projects from MATLAB

This example shows how to open a Polyspace project file with extension .psprj from MATLAB. In this example, open the project file Code_Prover_Example.psprj.

Assign the full project file path to a MATLAB variable prjFile.

prjFile = fullfile(polyspaceroot, 'polyspace', 'examples', 'cxx', ...
         'Code_Prover_Example', 'Code_Prover_Example.psprj');

Open the project.

polyspaceCodeProver(prjFile)

Open Polyspace Results from MATLAB

This example shows how to open a Polyspace results file from MATLAB. In this example, you open the results file from the folder polyspaceroot\polyspace\examples\cxx\Code_Prover_Example\Module_1\CP_Result.

Assign the full folder path to a MATLAB variable resFolder.

resFolder = fullfile(polyspaceroot, 'polyspace', 'examples', ...
       'cxx', 'Code_Prover_Example', 'Module_1', 'CP_Result');

Open the results.

polyspaceCodeProver('-results-dir',resFolder)

Run Polyspace Verification with Options Object

This example shows how to run a Polyspace verification in MATLAB using objects.

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', 'Code_Prover_Example', 'sources', 'single_file_analysis.c')};
opts.EnvironmentSettings.IncludeFolders = {fullfile(polyspaceroot, 'polyspace', 'examples',...
    'cxx', 'Code_Prover_Example', 'sources')};
opts.ResultsDir = fullfile(pwd,'results');

Run the verification and view the results.

polyspaceCodeProver(opts);
polyspaceCodeProver('-results-dir',opts.ResultsDir)

Run Polyspace Verification from MATLAB with DOS/UNIX Options

This example shows how to run a Polyspace verification in MATLAB using DOS/UNIX-style options.

Run the analysis and open the results.

sourceFiles = fullfile(polyspaceroot, 'polyspace', 'examples',...
    'cxx', 'Code_Prover_Example', 'sources', 'single_file_analysis.c');
includeFolders = fullfile(polyspaceroot, 'polyspace', 'examples',...
    'cxx', 'Code_Prover_Example', 'sources');
resultsDir = fullfile(pwd,'results');
polyspaceCodeProver('-sources',sourceFiles, ...
             '-I',includeFolders, ...
             '-results-dir',resultsDir,...
             '-main-generator');
polyspaceCodeProver('-results-dir',resultsDir);

Run Polyspace Verification with Coding Rules Checking

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.MisraC3Subset = 'mandatory';
opts.CodingRulesCodeMetrics.EnableMisraC3 = true;
opts.CodeProverVerification.EnableMain = true;
opts.InputsStubbing.DoNotGenerateResultsFor = 'all-headers';
polyspaceCodeProver(opts);
polyspaceCodeProver('-results-dir',resFolder1);

Verify coding rules with DOS/UNIX options.

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

Input Arguments

optsObject — Polyspace options object name

object handle

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.ModelLinkOptions.

Example: opts

projectFile — Name of .psprj file

character vector

Name of project file with extension .psprj, specified as a character vector.

If the file is not in the current folder, projectFile must include a full or relative path. To identify the current folder, use pwd. To change the current folder, use cd.

Example: 'C:\Polyspace_Projects\myProject.psprj'

resultsFile — Name of .pscp file

character vector

Name of results file with extension .pscp, specified as a character vector.

If the file is not in the current folder, resultsFile must include a full or relative path.

Example: 'myResults.pscp'

resultsFolder — Name of result folder

character vector

Name of result folder, specified as a character vector. The folder must contain the results file with extension .pscp. If the results file resides in a subfolder of the specified folder, this command does not open the results file.

If the folder is not in the current folder, resultsFolder must include a full or relative path.

Example: 'C:\Polyspace\Results\'

sourceFiles — Comma-separated names of .c or .cpp files

character vector

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.

Output Arguments

status — Status indicating whether the Polyspace Code Prover verification completed successfully or not

true | false

If the Code Prover verification completes without error, status is false. Otherwise, it is true.

The verification might fail for multiple reasons, including:

• You provided a source file, project file, or results file that does not exist.

• You specified an invalid path.

• One of your files did not compile.

jobID — ID of job associated with submitted analysis on the remote cluster

integer

If you offload the Polyspace analysis to a remote cluster, the command returns the ID of the job associated with the submitted analysis on the remote cluster. You can use this ID to manage the job or download the analysis results once the job completes. See also polyspaceJobsManager.

Version History

Introduced in R2013b