Main Content

polyspace-code-prover

(DOS/UNIX) Run a Code Prover verification from Windows, Linux, or other command line

collapse all in page

Syntax

polyspace-code-prover [options]
polyspace-code-prover -sources sourceFiles [options]
polyspace-code-prover -sources-list-file listOfSources [options]
polyspace-code-prover -options-file optFile
polyspace-code-prover -h[elp]

Description

Note

This Polyspace® command is available in polyspaceroot\polyspace\bin. Here, polyspaceroot is the Polyspace installation folder, for instance, C:\Program Files\Polyspace\R2024b (see also Installation Folder). To avoid typing the full path to this command, add this location to the PATH environment variable in your operating system.

polyspace-code-prover [options] runs a Code Prover verification if your current folder contains a sources subfolder with source files (.c or .cxx files). The verification considers files in sources and all subfolders under sources. You can customize the verification with additional options.

polyspace-code-prover -sources sourceFiles [options] runs a Code Prover verification on the source file(s) sourceFiles. You can customize the verification with additional options.

example

polyspace-code-prover -sources-list-file listOfSources [options] runs a Code Prover verification on the source files listed in the text file listOfSources. You can customize the verification with additional options.

polyspace-code-prover -options-file optFile runs a Code Prover verification with the options specified in the option file.

example

polyspace-code-prover -h[elp] lists a summary of possible analysis options.

Examples

collapse all

Run a local Code Prover verification by specifying analysis options in the command itself. This example uses source files from a demo Polyspace Code Prover example. To run this example, replace polyspaceroot with the path to your Polyspace installation, for example C:\Program Files\Polyspace\R2024b.

Run a verification on numerical.c and programming.c, checking for MISRA C:2012 mandatory rules and using GNU 4.7 compiler settings. This example command is split by ^ characters for readability. In practice, you can put all commands on one line.

polyspace-code-prover -lang C^
 -sources polyspaceroot\polyspace\examples\cxx\Code_Prover_Example\sources\*.c,^
 -I polyspaceroot\polyspace\examples\cxx\Code_Prover_Example\sources\^
 -compiler generic -misra3 mandatory^
 -author jlittle -prog myProject -results-dir C:\Polyspace_Workspace\Results\

Open the results.

polyspace C:\Polyspace_Workspace\Results\ps_results.pscp

To rerun the verification, you must rerun it from the command line.

Run a verification by using an options file to specify your source files and analysis options. To run this example, replace polyspaceroot with the path to your Polyspace installation, for example C:\Program Files\Polyspace\R2024b.

Save this text to a text file called myOptsFile.txt.

# Polyspace analysis options 
-I polyspaceroot\polyspace\examples\cxx\Code_Prover_Example\sources
-verif-version 1.0
-sources polyspaceroot\polyspace\examples\cxx\Code_Prover_Example\sources\*.c
-lang C
-target i386
-compiler generic
-dos
-do-not-generate-results-for all-headers
-misra3 mandatory-required
-entry-points proc1,proc2,server1,server2,tregulate
-critical-section-begin Begin_CS:Cs10
-critical-section-end End_CS:Cs10
-temporal-exclusions-file polyspaceroot\polyspace\examples\cxx\Code_Prover_Example\sources\temporal_exclusions.txt
-float-rounding-mode to-nearest
-signed-integer-overflows forbid
-unsigned-integer-overflows allow
-uncalled-function-checks none
-check-subnormal allow
-O2
-to Software Safety Analysis level 2
-context-sensitivity-auto
-path-sensitivity-delta 0
-author jlittle 
-prog myProject 
-results-dir C:\Polyspace_Workspace\Results\

Run the verification with the options specified in the text file.

polyspace-code-prover -options-file myOptsFile.txt

Open the results.

polyspace C:\Polyspace_Workspace\Results\ps_results.pscp

To rerun the verification, you must rerun it from the command line.

Input Arguments

collapse all

Comma-separated C or C++ source file names, specified as a string. If the files are not in the current folder (pwd), sourceFiles must include a full or relative path. To avoid errors because of paths with spaces, add quotes " " around the path. For more information, see -sources.

If your current folder contains a sources subfolder with the source files, you can omit the -sources flag. The verification considers files in sources and all subfolders under sources.

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

Text file which lists the name of C or C++ files, specified as a string. If the files are not in the current folder (pwd), listOfSources must include a full or relative path. To avoid errors because of paths with spaces, add quotes " " around the path. For more information, see -sources-list-file.

Example: filename.txt, "C:\ps_analysis\source_files.txt"

Analysis options and their corresponding values, specified by the option name and if applicable value. For syntax specifications, see the individual analysis option reference pages.

Example: -lang C-CPP, -target i386

Text file listing analysis options and values, specified as a string. For more information, see -options-file.

Example: opts.txt, "C:\ps_analysis\options.txt"

Tips

If you run the command as part of a script, check the exit status to confirm a successful analysis. The command returns zero on a successful analysis. A nonzero return value means that the analysis failed and was not completed. For instance, if the analyzed file does not compile, the command returns a nonzero value. If some of the files do not compile when you are analyzing multiple files, the command completes analysis on the files that do compile and returns zero. It is possible to stop analysis if a file does not compile. See Stop analysis if a file does not compile (-stop-if-compile-error).

After running the command, you can check the %ERRORLEVEL% variable in Windows command line to confirm a successful analysis.

Version History

Introduced in R2013b

See Also

Topics