Run Polyspace Analysis from Command Line

To run an analysis from a DOS or UNIX^® command window, use the command polyspace-bug-finder or polyspace-code-prover followed by other options you want to use. See also:

• polyspace-bug-finder

• polyspace-code-prover (Polyspace Code Prover)

To save typing the full path to the commands, add the path polyspaceroot\polyspace\bin to the Path environment variable on your operating system. Here, polyspaceroot is the Polyspace installation folder, for instance, C:\Program Files\Polyspace\R2024b. See also Installation Folder.

Specify Sources and Analysis Options Directly

At the Windows^®, Linux^® or Mac OS X command-line, append sources and analysis options to the polyspace-bug-finder or polyspace-code-prover command.

For instance:

• To specify sources, use the -sources option followed by a comma-separated list of sources.

  polyspace-bug-finder -sources C:\mySource\myFile1.c,C:\mySource\myFile2.c

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

• To specify the target processor, use the -target option. For instance, to specify the m68k processor for your source file file.c, use the command:

  polyspace-bug-finder -sources "file.c" -lang c -target m68k

• To check for violation of MISRA C™ rules, use the -misra2 option. For instance, to check for only the required MISRA C rules on your source file file.c, use the command:

  polyspace-bug-finder -sources "file.c" -misra2 required-rules

• To specify a results folder, use the option -results-dir.

  Note that by default, the results folder is cleaned up and repopulated at each run. To avoid accidental removal of files during the cleanup, instead of using an existing folder that contains other files, specify a dedicated folder for the Polyspace^® results.

• Optionally, specify an analysis id by using the option -verif-version. You can use this id to refer to different runs of the analysis. For example, you can import comments from a specific run of the analysis by using the id. This id is also reported as the version for the generated report.

For the full list of analysis options, see:

• Complete List of Polyspace Bug Finder Analysis Engine Options

• Complete List of Polyspace Code Prover Analysis Options (Polyspace Code Prover)

For the full list of options, enter the following at the command line:

polyspace-bug-finder -help

Specify Sources and Analysis Options in Text File

Instead of specifying the options directly, you can save the options in a text file and use the text file each time you run the analysis.

1. Create an options file called listofoptions.txt with your options. For example:

   #These are the options for MyCodeProverProject
   -lang c
   -prog MyCodeProverProject
   -author jsmith
   -sources "mymain.c,funAlgebra.c,funGeometry.c"
   -target x86_64
   -compiler generic
   -dos
   -misra2 required-rules
   -do-not-generate-results-for all-headers
   -main-generator
   -results-dir C:\Polyspace\MyCodeProverProject
   -ver-f-version 1.0

2. Run Polyspace using options in the file listofoptions.txt.

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

See also -options-file.

Create Options File from Build System

If you use a build command (makefile) to build your source code, you can collect the sources and compiler options from your build command. Trace your build command to generate a text file with the required Polyspace options.

1. Create a list of Polyspace options using the configuration tool.

   polyspace-configure -output-options-file \
           myOptions buildCommand

   where buildCommand is the command you use to build your source code, for instance make -B.

   See also polyspace-configure.

2. Run Polyspace using the options read from your build.

   polyspace-bug-finder -options-file myOptions \
           -results-dir myResults
   

   In addition to the options collected from your build command, you might want to add further options, for instance, to specify the defect checkers. You can append these options to the options file, add them directly at the command line or add them through a second options file (using another -options-file flag).

3. Open the results in the Polyspace user interface.

   polyspace-bug-finder myResults