polyspace-configure

(DOS/UNIX) Create Polyspace project from your build system at the DOS or UNIX command line

Syntax

polyspace-configure buildCommand

polyspace-configure [options] buildCommand

polyspace-configure [options] -compilation-database jsonFile

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 for desktop products or Installation Folder for server products). To avoid typing the full path to this command, add this location to the PATH environment variable in your operating system.

polyspace-configure buildCommand traces your build system and creates a Polyspace project with information gathered from your build system. Polyspace creates a project from your build system only if your build commands or makefiles meet certain requirements. For a list of compiler and build command requirements, including a list of compilers that Polyspace supports, see Requirements for Project Creation from Build Systems.

polyspace-configure [options] buildCommand traces your build system and uses options to modify the default operation of polyspace-configure. Specify the modifiers before buildCommand, otherwise they are considered as options in the build command itself.

polyspace-configure [options] -compilation-database jsonFile creates a Polyspace project with information gathered from the JSON compilation database file jsonFile that you provide. You do not need to specify a build command or trace your build system. For more on JSON compilation databases, see JSON Compilation Database.

Examples

Create Polyspace Project Using Compile Command (gcc, cl, etc.)

This example shows how to use a compile command to create your Polyspace project. The simplest way to run polyspace-configure is to run it directly on the compile command used to build your source code. This example uses the GCC compiler and the compile command gcc. GCC is a standard compiler suite included with Linux^® based systems. For Windows^® based systems, MinGW can be installed to support the GCC compiler.

First, ensure that your source code compiles without errors.

gcc myFilename.c otherFile.c

After confirming that your source code compiles without errors, remove the object files before continuing.

rm myFilename.o otherFile.o

Create a Polyspace project specifying a unique project name. Run polyspace-configure on the compile command as previously tested.

polyspace-configure -prog myProject gcc myFilename.c otherFile.c

Open the Polyspace project in the Polyspace user interface.

If you use Visual Studio^® to compile your sources, you can replace gcc in the above example with cl. You can also run polyspace-configure on a full build of your Visual Studio project. See Create Polyspace Projects from Visual Studio Build.

Note that polyspace-configure creates a new Polyspace project using the sources from your compile command. It is not possible to append to an already existing Polyspace project by using the polyspace-configure command. If you use compile options (such as -D for gcc), polyspace-configure sets the equivalent Polyspace options in the project. For more details, see Algorithms.

Create Polyspace Platform Project Using Compile Command (gcc, cl, etc.)

This example shows how to use a compile command to create a Polyspace Platform (Polyspace Test) project. The simplest way to run polyspace-configure is to run it directly on the compile command used to build your source code. This example uses the GCC compiler and the compile command gcc. GCC is a standard compiler suite included with Linux based systems. For Windows based systems, MinGW can be installed to support the GCC compiler.

First, ensure that your source code compiles without errors.

gcc myFilename.c otherFile.c

After confirming that your source code compiles without errors, remove the object files before continuing.

rm myFilename.o otherFile.o

Create a Polyspace Platform project specifying a unique project name. Run polyspace-configure on the compile command as previously tested.

polyspace-configure -output-platform-project myProject gcc myFilename.c otherFile.c

Open the Polyspace project in the Polyspace Platform user interface.

If you use Visual Studio to compile your sources, you can replace gcc in the above example with cl. You can also run polyspace-configure on a full build of your Visual Studio project. See Create Projects from Visual Studio in Polyspace Platform User Interface (Polyspace Test).

Create Polyspace Project from Makefile

Typically, in real applications, you do not invoke the compiler directly to build your source code. Your build command runs several commands, one of which is compilation. For instance, you might be running a makefile to build your source code. This example shows how to create a Polyspace project if you use the command make targetName buildOptions to build your source code.

Create a Polyspace project specifying a unique project name. Use the -B or -W makefileName option with make so that all the prerequisite targets in the makefile are remade.

polyspace-configure  -prog myProject \
make -B targetName buildOptions

Open the Polyspace project in the Polyspace user interface.

Create Polyspace Options File from JSON Compilation Database

This example shows how to create a Polyspace options file from a JSON compilation database that you generate with the CMake build system generator. CMake generates build instructions for the build tool you specify, such as a UNIX^® Makefiles for make or project files for Microsoft^® Visual Studio. CMake supports the generation of a JSON compilation database only for Makefile generators and Ninja generator. For more information, see makefile generators.

Generate a JSON compilation database for your CMake project. For an example of a Cmake project, see polyspaceroot\polyspace\examples\doc_cxx\compilation_database where polyspaceroot is your Polyspace installation folder.

Navigate to the root of your project source tree. This folder contains the file CMakeLists.txt which CMake uses as an input to generate build instructions. Enter these commands:

mkdir JSON_cdb
cd JSON_cdb
cmake -G "Unix Makefiles" -DCMAKE_EXPORT_COMPILE_COMMANDS=1 ../

The last command generates a UNIX makefile with build instructions for the make build tool. The command also outputs file compile_commands.json. This file lists the compiler calls for every translation unit in your project.

Generate a Polyspace options file from the compilation database that you generated in the previous step.

polyspace-configure -compilation-database compile_commands.json \
-output-options-file options.txt

You do not need to specify a build command and polyspace-configure does not trace your build. Polyspace extracts information about your build system from the JSON compilation database.

Pass the options file to Polyspace to run an analysis, for instance:

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

Create Projects That Have Different Source Files from Same Build Trace

This example shows how to create different Polyspace projects from the same trace of your build system. You can specify which source files to include for each project.

Trace your build system without creating a Polyspace project by specifying the option -no-project. To ensure that all the prerequisite targets in your makefile are remade, use the appropriate make build command option, for instance -B.

polyspace-configure -no-project make -B

polyspace-configure stores the cache information and the build trace in default locations inside the current folder. To store the cache information and build trace in a different location, specify the options -cache-path and -build-trace.

Generate Polyspace projects by using the build trace information from the previous step. Specify a project name and use the -include-sources or -exclude-sources option to select which files to include for each project.

polyspace-configure -no-build -prog myProject \
-include-sources "glob_pattern"

glob_pattern is a glob pattern that corresponds to folders or files you filter in or out of your project. To ensure the shell does not expand the glob patterns you pass to polyspace-configure, enclose them in double quotes. For more information on the supported syntax for glob patterns, see Select Files for Polyspace Analysis Using Pattern Matching.

If you specified the options -build-trace and -cache-path in the previous step, specify them again.

Delete the trace file and cache folder.

rm -r polyspace_configure_cache polyspace_configure_build_trace
 

If you used the options -build-trace and -cache-path, use the paths and file names from those options.

Run Command-Line Polyspace Analysis from Makefile

This example shows how to run Polyspace analysis if you use the command make targetName buildOptions to build your source code. In this example, you use polyspace-configure to trace your build system but do not create a Polyspace project. Instead you create an options file that you can use to run Polyspace analysis from command-line.

Create a Polyspace options file specifying the -output-options-file command. Use the -B or -W makefileName option with make so that all prerequisite targets in the makefile are remade.

polyspace-configure -output-options-file\
 myOptions make -B targetName buildOptions

Use the options file that you created to run a Polyspace analysis at the command line:

polyspace-code-prover -options-file myOptions

Input Arguments

buildCommand — Command for full build of source code

string

Build command specified exactly as you use to build your source code.

The build command must perform a full build of your sources and not an incremental build. Typically, build commands such as make are set up to only build sources that have changed since the previous build. However, polyspace-configure requires a full build to determine which sources to add to a Polyspace project or options file. Add appropriate options to your build command to force a full build. For instance, when using a makefile, append the option -B to make.

Example: make -B, make -B -W makefileName

options — Options for changing default operation of polyspace-configure

single option starting with -, followed by argument | multiple space-separated option-argument pairs

Basic Options — Options for output and debugging

string

Option	Description
-prog projectName	Project name that appears in the Polyspace user interface. The default is polyspace. If you do not use the option -output-project, the -prog argument also sets the project name. Example: -prog myProject creates a project that has the name myProject in the user interface. If you do not use the option -output-project, the project name is also myProject.psrprj.
-author authorName	Name of project author. Example: -author jsmith
-output-project filePath	Path to Polyspace project file. The default is the file polyspace.psprj in the current folder. Example: -output-project ../myProjects/project1 creates a project project1.psprj in the folder with the relative path ../myProjects/.
-output-platform-project filePath	Path to Polyspace Platform project file or workspace file (if you use one of the options -module, -modules-list, or -module-output-pattern). Polyspace saves the file in the current folder. Example:-output-platform-project ../myProjects/project1 creates a project project1.psprjx in the folder with the relative path ../myProjects/. Example:-output-platform-project ../myProjects/workspace1 -module creates a workspace file project1.pswkps in the folder with the relative path ../myProjects/. For more information on Polyspace Platform projects, see: Create Project and Add Source Files in Polyspace Platform User Interface Manage Related Projects in Polyspace Platform User Interface Using Workspaces
-update-platform-project filePath	Use this option to update the build configuration of a Polyspace Platform project (.psprjx) using the configuration of the current project run. The filePath argument can be relative or absolute. If a processor configuration already exists, the command uses that configuration for the new build configuration. If the specified project does not exist, the command creates a new project. Example: polyspace-configure -update-platform-project ../myProjects/myProject.psprjx
-output-options-file filePath	Path of analysis options file that Polyspace generates. Use this file for command-line analysis using one of these commands: polyspace-bug-finder polyspace-code-prover polyspace-bug-finder-server polyspace-code-prover-server polyspace-bug-finder-access
-allow-build-error	Option to create a Polyspace project even if an error occurs in the build process. If an error occurs, the build trace log shows the following message: polyspace-configure (polyspaceConfigure) ERROR: build command command_name fail [status=status_value] command_name is the build command name that you use and status_value is the non-zero exit status or error level that indicates which error occurred in your build process. This option can create a useful project if your build command builds the source files but exits with a non-zero exit status. If your source files do not compile and the build fails, resolve your build failure before using polyspace-configure again. This option is ignored when you use -compilation-database.
-allow-overwrite	Option to overwrite a project with the same name, if it exists. By default, polyspace-configure (polyspaceConfigure) throws an error if a project with the same name already exists in the output folder. Use this option to overwrite the project.
-no-console-output -silent (default) -verbose	Option to suppress or display additional messages from running polyspace-configure (polyspaceConfigure). -no-console-output – Suppress all outputs including errors and warnings. -silent (default) – Show only errors and warnings. -verbose – Show all messages. If you specify more than one of these options, the most verbose option is applied. Polyspace ignores these options when you use them in combination with -easy-debug.
-help	Option to display the full list of polyspace-configure (polyspaceConfigure) commands
-debug	Option to store debug information for use by MathWorks® technical support. This option has been superseded by the option -easy-debug.
-easy-debug folderPath	Path of folder where Polyspace stores debug information for use by MathWorks technical support. After a polyspace-configure (polyspaceConfigure) run, the folder folderPath contains a zipped file ending with pscfg-output.zip. If the run fails to create a complete Polyspace project or options file, send this zipped file to MathWorks Technical Support for further debugging. The zipped file does not contain source files traced in the build. See also Errors in Project Creation from Build Systems.

Multiple Modules Creation Options — Create separate output per module

string

These options are not compatible with -compilation-database

Option	Description
-module	Option to create a separate analysis module for each binary that you create in a build system. What constitutes an analysis module depends on the output of the polyspace-configure command: If you use the option -module with the option -output-project projectName, the command generates a file projectName.psprj with one module per binary. If you use the option -module with the option -output-options-path pathName, the command generates one options file per binary in the folder pathName. If you use the option -module with the option -output-platform-project workspaceName, Polyspace creates a workspace file (workspaceName.pswks) with one Polyspace Platform project (.psprjx) per binary. For more information on workspaces, see Manage Related Projects in Polyspace Platform User Interface Using Workspaces. This option is supported only in the following cases: If you create a project or options file from a build command using one of these linkers: GNU® — ld, gold, or ar linkers. Visual C++® — link.exe linker. If you create a project or options file from a CMake JSON compilation database. Note that when you create a separate options file for each binary in this way, each options file contains source files directly involved in the binary and not through shared objects. For more information, see Modularize Polyspace Analysis by Using Build Command.
-modules-list fileWithModuleList	Option to create a separate output for each root folder you state in the text file fileWithModuleList. Specify one root folder per line in the text file. For each root folder listed in the text file, the polyspace-configure command creates a separate analysis module that consists of only the source files in that root folder. Root folder paths are resolved with respect to the current working folder unless you use the option -project-root. What constitutes an analysis module depends on the output of the polyspace-configure command: If you use the option -modules-list with the option -output-options-path pathName, the command generates one options file per root folder in the folder pathName. If you use the option -modules-list with the option -output-platform-project workspaceName, Polyspace creates a workspace file (workspaceName.pswks) with one Polyspace Platform project (.psprjx) per root folder. For more information on workspaces, see Manage Related Projects in Polyspace Platform User Interface Using Workspaces. This option is supported whether you create a project or options file from a build command or a JSON compilation database.
-module-output-pattern regex	Option to create a separate output for each root folder captured by the regular expression regex. Specify a capturing group in the regular expression. For each root folder captured by the regular expression, the polyspace-configure command creates a separate analysis module that consists of only the source files in that root folder. Root folder paths are resolved: With respect to the folder from which you run the build command, if you create analysis modules from a build command. With respect to the directory entry in your JSON compilation database, if you create analysis modules from a JSON compilation database. What constitutes an analysis module depends on the output of the polyspace-configure command: If you use the option -module-output-pattern with the option -output-options-path pathName, the command generates one options file per root folder in the folder pathName. If you use the option -module-output-pattern with the option -output-platform-project workspaceName, Polyspace creates a workspace file (workspaceName.pswks) with one Polyspace Platform project (.psprjx) per root folder. For more information on workspaces, see Manage Related Projects in Polyspace Platform User Interface Using Workspaces. This option is supported whether you create a project or options file from a build command or a JSON compilation database.
-output-options-path folderPath	Path to folder where generated options files are saved. Use this option together with the option -module. The options files are named after the binaries created in the build system.
-project-root folderPath	Path to folder with respect to which root folder paths are resolved. Use this option together with the option -module-list. If you omit this option, root folder paths in the text file provided with -module-list are resolved with respect to the current working folder.

Advanced Options — Specify advanced configuration options

string

Option	Description
-compilation-database filePath	Path of JSON compilation database (JSON CDB) file. You generate this file from your build system, for instance by using the flag -DCMAKE_EXPORT_COMPILE_COMMANDS=1 with cmake. The file contains compiler calls for all the translation units in your projects. For more information, see JSON Compilation Database. polyspace-configure uses the content of this file to get information about your build system. The extracted compiler paths in the JSON CDB must be accessible from the path where you run polyspace-configure. You do not specify a build command when you use this option. These build systems and compilers support the generation of a JSON CDB: CMake Bazel Clang Ninja Qbs waf This option is not compatible with -no-project and with the options to create multiple modules. Polyspace ignores the cache control options -allow-build-error and -no-build when you use this option.
-compiler-config filePath	Path of compiler configuration file. The file must be in a specific format. For guidance, see the existing configuration files in polyspaceroot\polyspace\configure\compiler_configuration\. For information on the contents of the file, see Create Polyspace Projects from Build Systems That Use Unsupported Compilers. Example: -compiler-config myCompiler.xml
-no-project	Option to trace your build system without creating a Polyspace project and save the build trace information. Use this option to save your build trace information for a later run of polyspace-configure (polyspaceConfigure) with the -no-build option. This option is not compatible with -compilation-database.
-no-build	Option to create a Polyspace project using previously saved build trace information. To use this option, you must have the build trace information saved from an earlier run of polyspace-configure (polyspaceConfigure) with the -no-project option. If you use this option, you do not need to specify the buildCommand argument. This option is ignored when you use -compilation-database.
-no-sources	Option to create a Polyspace options file that does not contain the source file specifications. Use this option when you intend to specify the source files by other means. For instance, you can use this option when: Running Polyspace on AUTOSAR-specific code. You want to create an options file that traces your build command for the compiler options: -output-options-file options.txt -no-sources You later append this options file when extracting source file names from ARXML specifications and running the subsequent Code Prover analysis with polyspace-autosar -extra-options-file options.txt See also Run Polyspace on AUTOSAR Code Using Build Command. Running Polyspace in Eclipse™. Your source files are already specified in your Eclipse project. When running a Polyspace analysis, you want to specify an options file that has the compilation options only.
-extra-project-options polyspaceAnalysisOpts	Options that are used for subsequent Polyspace analysis. Once a Polyspace project is created, you can change some of the default options in the project. Alternatively, you can pass these options when tracing your build command. The flag -extra-project-options allows you to pass additional options. Specify multiple options in a space separated list, for instance "-allow-negative-operand-in-shift -stubbed-pointers-are-unsafe". Suppose you have to set the option -stubbed-pointers-are-unsafe for every Polyspace project created. Instead of opening each project and setting the option, you can use this flag when creating the Polyspace project: -extra-project-options "-stubbed-pointers-are-unsafe" For the list of options available, see: Complete List of Polyspace Bug Finder Analysis Engine Options Complete List of Polyspace Code Prover Analysis Options If you are creating an options file instead of a Polyspace project from your build command, do not use this flag. Instead, add the extra analysis options manually in the generated options file, in a separate options file, or at the command-line when you start the analysis.
-tmp-path folderPath	Path of folder where temporary files are stored.
-build-trace filePath	Path of file where build information is stored. The default is ./polyspace_configure_build_trace.log. Example: -build-trace ../build_info/trace.log
-log filePath	Path of log file where the output of the polyspace-configure command is stored. The use of this option does not suppress the console output.
-include-sources glob pattern -exclude-sources glob pattern	Option to specify which source files polyspace-configure (polyspaceConfigure) includes in, or excludes from, the generated project. You can combine both options together. A source file is included if the file path matches the glob pattern that you pass to -include-sources. A source file is excluded if the file path matches the glob pattern that you pass to -exclude-sources.
-print-included-sources -print-excluded-sources	Option to print the list of source files that polyspace-configure (polyspaceConfigure) includes in, or excludes from, the generated project. You can combine both options together. The output displays the full path of each file on a separate line. Use this option to troubleshoot the glob patterns that you pass to -include-sources or -exclude-sources. You can see which files match the pattern that you pass to -include-sources or -exclude-sources.
-compiler-cache-path folderPath	Specify a folder path where polyspace-configure looks for or stores the compiler cache files. If the folder does not exist, polyspace-configure creates it. By default, Polyspace looks for and stores compiler caches under these folder paths: Windows %appdata%\Mathworks\R2024b\Polyspace Linux ~/.matlab/R2024b/Polyspace Mac ~/Library/Application Support/MathWorks/MATLAB/R2024b/Polyspace
-no-compiler-cache	Use this option if you do not want Polyspace to cache your compiler configuration information or to use an existing cache for your compiler configuration. By default, the first time you run polyspace-configure with a particular compiler configuration, Polyspace queries your compiler for the size of fundamental types, compiler macro definitions, and other compiler configuration information then caches this information. Polyspace reuses the cached information in subsequent runs of polyspace-configure for builds that use the same compiler configuration.
-reset-compiler-cache-entry	Use this option to query the compiler for the current configuration and to refresh the entry in the cache file that corresponds to this configuration. Other compiler configuration entries in the cache are not updated.
-clear-compiler-cache	Use this option to delete all compiler configurations stored in the cache file. If you also specify a build command or -compilation-database, polyspace-configure computes and caches the compiler configuration information of the current run, except if you specify -no-project or -no-compiler-cache.
-import-macro-definitions none | from-allowlist | from-source-tokens | from-compiler	Typically, you do not need to specify this option. Polyspace attempts to automatically determine the best strategy to query your compiler for macro definitions in this order of priority: from-compiler — Polyspace uses native compiler options, such as gcc -dm -E, to obtain the compiler macro definitions. This strategy does not require Polyspace to trace your build and is available only for compilers that support listing macro definitions. from-source-tokens — Polyspace uses every non-keyword token in your source code to query your compiler for macro definitions. This strategy is available only if Polyspace can trace your build. The strategy is not available if you use option -compilation-database. from-allowlist — Polyspace uses an internal allow list to query the compiler for macro definitions. If you prefer to specify macro definitions manually, use this option with the none flag and use option Preprocessor definitions (-D) to specify the macro definitions. If the macro import strategy that Polyspace uses is not the one that you expect, try specifying this option manually to troubleshoot the issue.
-options-for-sources-delimiter delimCharacter	Specify the character to use as a separator between analysis options when Polyspace generates an options file associated with one source file using the option -options-for-sources. Typically, the option -options-for-sources uses the ; character (semicolon) as a separator between analysis options in the generated file. See also -options-for-sources.

Cache Control Options — Generate cache options for debugging

string

These options are primarily useful for debugging. Use the options if polyspace-configure (polyspaceConfigure) fails and MathWorks Technical Support asks you to use the option and provide the cached files. Starting R2020a, the option -easy-debug provides an easier way to provide debug information. See Contact Technical Support About Issues with Running Polyspace.

Polyspace ignores these options when you use -compilation-database.

Option	Description
-no-cache -cache-sources (default) -cache-all-text -cache-all-files	Option to perform one of the following: -no-cache: Not create a cache -cache-sources: Cache text files temporarily created during build for later use by polyspace-configure (polyspaceConfigure). -cache-all-text: Cache all text files including sources and headers. -cache-all-files: Cache all files including binaries. Typically, you cache temporary files created by your build command to debug issues in tracing the command.
-cache-path folderPath	Path of folder where cache information is stored. When tracing a Visual Studio build (devenv.exe), if you see the error: path is too long try using a shorter path for this option to work around the error. Example: -cache-path ../cache
-keep-cache -no-keep-cache (default)	Option to preserve or clean up cache information after polyspace-configure (polyspaceConfigure) completes execution. If polyspace-configure (polyspaceConfigure) fails, you can provide this cache information to technical support for debugging purposes.

Algorithms

The polyspace-configure command creates a Polyspace project or options file from a build command such as make using roughly these steps:

1. The build command is first executed. polyspace-configure keeps track of the commands that run during this build and the files read or written. One or more of these commands would be the compiler invocation. For instance, if the build command uses a GCC compiler, one or more of these commands would exercise the gcc, g++, or related executable. Based on the presence of a known compiler executable, polyspace-configure picks out the compiler invocation commands from amidst all the commands executed during build.

2. Each compiler invocation command contains these three parts: the compiler executable, some source files and some compiler options. For instance, the following command exercises the GCC compiler on the file myFile.c with a compiler option -std that triggers C++11-based compilation:

   gcc -std=c++11 myFile.c

   polyspace-configure reads the source file names from these commands and directly uses them in the Polyspace project or options file. The compiler executable and compiler options are translated to Polyspace analysis options.

   To determine Polyspace options such as the ones corresponding to sizes of basic types or underlying type of size_t, polyspace-configure runs the previously read compiler executable plus compiler options on some small source files. Depending on whether a source file compiles successfully or shows errors, polyspace-configure can set an appropriate Polyspace option. To determine compiler macro definitions and include paths, polyspace-configure also reinvokes the compiler on small sources but thereafter uses a slightly different strategy.

   For a simple example of a source file that can help determine a Polyspace option, see the reference page for the option Management of size_t (-size-t-type-is).

Instead of a build command, polyspace-configure can also create a project or options file from a JSON compilation database. When the polyspace-configure command runs on a compilation database, the first step above is omitted. A compilation database directly states the compiler invocation command in entries such as this:

{
"directory": "/proj/files/
"command": "/usr/local/bin/gcc -std=c++11 -c /proj/files/myFile.c",
"file" : "/proj/files/myFile.c"
}

polyspace-configure can simply read these compiler invocation commands and continue with the remaining step of reinvoking the compiler on small source files. Since the build command execution step is skipped, running polyspace-configure on a compilation database is much faster than running polyspace-configure on a build command. However, it is your responsibility to make sure that the compilation database you provide accurately reflects a full build of your source code.

Version History

Introduced in R2013b