polyspace-configure
(System Command) Create Polyspace Platform project, workspace, or options file from build command or compilation database
Syntax
Description
The polyspace-configure system command creates a Polyspace® Platform project or options file from a build command or compilation database.
Create Project
polyspace-configure [-output-platform-project|-update-platform-project] creates a Polyspace Platform project (psPlatformProject [options] buildCommand.psprjx file) using information gathered from executing the command buildCommand.
If you use the option
-output-platform-project, the command creates a new project.If you use the option
-update-platform-project, the command updates an existing project by overwriting auto-generated information such as automatically added sources and build configuration, and retaining manually added information such as static analysis configuration and tests.
If you create a project from a build command using polyspace-configure, the build command must be the last entry. Any option following the build command is considered as an option for the build command and not a polyspace-configure option.
polyspace-configure [-output-platform-project|-update-platform-project] creates a Polyspace Platform project using information gathered from the JSON compilation database file specified by psPlatformProject -compilation-database jsonFile [options]jsonFile.
Create Workspace with Multiple Projects for Multiple Components
polyspace-configure -module [-output-platform-project|-update-platform-project] creates or updates a Polyspace Platform workspace (psPlatformWorkspace [options] buildCommand.pswks file) using information from buildCommand. Each project in the workspace corresponds to one binary created by the build command and includes sources directly involved in creating the binary. The option -module is supported only if your build command uses GNU® or Visual C++® linkers.
polyspace-configure -modules-list creates or updates a Polyspace Platform workspace (fileWithModulesList [-project-root commonRootFolder] [-output-platform-project|-update-platform-project] psPlatformWorkspace [options] buildCommand.pswks file) using information from buildCommand. If the file fileWithModulesList lists multiple root folders with one folder per line, each project in the workspace includes all sources residing under one such root folder. If the folder paths are not absolute, they are resolved with respect to the current folder unless you use the option -project-root.
polyspace-configure -module-output-pattern creates or updates a Polyspace Platform workspace (regexPattern [-output-platform-project|-update-platform-project] psPlatformWorkspace [options] buildCommand.pswks file) using information from buildCommand. If the regular expression regexPattern contains a capturing group capturing multiple root folders, each project in the workspace includes all sources residing under one such root folder. If the folder paths are not absolute, they are resolved with respect to the current folder.
polyspace-configure -modules-list creates or updates a Polyspace Platform workspace (fileWithModulesList [-project-root commonRootFolder] [-output-platform-project|-update-platform-project] psPlatformWorkspace -compilation-database jsonFile [options].pswks file) using information from a compilation database jsonFile. If the file fileWithModulesList lists multiple root folders with one folder per line, each project in the workspace includes all sources residing under one such root folder. If the folder paths are not absolute, they are resolved with respect to the current folder unless you use the option
-project-root.
polyspace-configure -module-output-pattern creates or updates a Polyspace Platform workspace (regexPattern [-output-platform-project|-update-platform-project] psPlatformWorkspace -compilation-database jsonFile [options].pswks file) using information from a compilation database jsonFile. If the regular expression regexPattern contains a capturing group capturing multiple root folders, each project in the workspace includes all sources residing under one such root folder. If the folder paths are not absolute, they are resolved with respect to the directory entry in the compilation
database.
Create Options File
polyspace-configure -output-options-file creates an options file for Polyspace static analysis using information gathered from executing the command optionsFile [options] buildCommandbuildCommand.
polyspace-configure -output-options-file creates an options file for Polyspace static analysis using information gathered from the JSON compilation database file specified by optionsFile -compilation-database jsonFile [options]jsonFile.
Create Multiple Options Files for Multiple Components
polyspace-configure -module -output-options-path creates multiple options files for static analysis in optionsFolder [options] buildCommandoptionsFolder using information from buildCommand. Each options file corresponds to one binary created by the build command and lists sources directly involved in creating the binary. The option
-module is supported only if your build command uses GNU or Visual C++ linkers.
polyspace-configure -modules-list creates multiple options files for static analysis in fileWithModulesList [-project-root commonRootFolder] -output-options-path optionsFolder [options] buildCommandoptionsFolder using information from buildCommand. If the file fileWithModulesList lists
multiple root folders with one folder per line, each generated options file lists sources residing under one such root folder. If the folder paths are not absolute, they are resolved with respect to the current working folder unless you use the option -project-root.
polyspace-configure -module-output-pattern creates multiple options files for static analysis in regexPattern -output-options-path optionsFolder [options] buildCommandoptionsFolder using information from buildCommand. If the regular expression regexPattern contains a capturing group capturing multiple root
folders, each generated options file lists sources residing under one such root folder. If the folder paths are not absolute, they are resolved with respect to the current folder.
polyspace-configure -modules-list creates multiple options files for static analysis in fileWithModulesList [-project-root commonRootFolder] -output-options-path optionsFolder -compilation-database jsonFile [options]optionsFolder using information from a compilation database jsonFile. If the file
fileWithModulesList lists multiple root folders with one folder per line, each project in the workspace includes all sources residing under one such root folder. If the folder paths are not absolute, they are resolved with respect to the current folder unless you use the option -project-root.
polyspace-configure -module-output-pattern creates multiple options files for static analysis in regexPattern -output-options-path optionsFolder -compilation-database jsonFile [options]optionsFolder using information from a compilation database jsonFile. If the regular expression regexPattern contains a
capturing group capturing multiple root folders, each generated options file lists sources residing under one such root folder. If the folder paths are not absolute, they are resolved with respect to the directory entry in the compilation database.
Examples
Input Arguments
Algorithms
The polyspace-configure command creates a Polyspace project or options file from a build command such as make using roughly these steps:
The build command is first executed.
polyspace-configurekeeps 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 thegcc,g++, or related executable. Based on the presence of a known compiler executable,polyspace-configurepicks out the compiler invocation commands from amidst all the commands executed during build.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.cwith a compiler option-stdthat triggers C++11-based compilation:gcc -std=c++11 myFile.c
polyspace-configurereads 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-configureruns 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-configurecan set an appropriate Polyspace option. To determine compiler macro definitions and include paths,polyspace-configurealso 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.