Create Polyspace Analysis Configuration from Build Command (Makefile)

To run Polyspace^® with scripts at regular intervals, for instance, on a server during continuous integration, you must configure all analysis options beforehand so that the analysis completes without errors. These options must be updated as necessary to keep up with new code submissions. If you use existing artifacts such as a build command (makefile) to build new code submissions, you can reuse the build command to configure a Polyspace analysis and stay updated with new submissions. With the polyspace-configure command, you can monitor the execution of a build command and create an options file for analysis with Polyspace.

This topic shows a simple tutorial illustrating how to create an options file from a build command and use the file for the subsequent analysis. The topic uses a Linux^® makefile and the GCC compiler, but you can adapt the commands to other operating systems such as Windows^® and other compilers such as Microsoft^® Visual Studio^®.

Copy the demo source files from polyspaceserverroot\polyspace\examples\cxx\Bug_Finder_Example\sources to a folder with write permissions. Here, polyspaceserverroot is the root installation folder of the Polyspace server products, for instance, C:\Program Files\Polyspace Server\R2019a.
Create a simple makefile that compiles the demo source files. Save the makefile in the same folder as the source files.
For instance, create a file named makefile and add this content:
```
CC := gcc
SOURCES := $(wildcard *.c)

all: $(CC) -c $(SOURCES)
```
Check that the makefile builds the source files successfully. Open a command terminal, navigate to the folder (using cd) and enter:
```
make -B
```
The make command should complete execution without errors.
The -B option ensures that all targets in the makefile are built. 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.
Trace the build command with polyspace-configure and create an options file compile_opts.
```
polyspace-configure -output-options-file compile_opts make -B
```
Create a second options file with additional options. For instance, create a file run_opts with this content:
```
-checkers numerical
-report-template BugFinder
-output-format pdf
```
The options run all numerical checkers in Bug Finder and creates a PDF report after analysis using the BugFinder template.
Run a Bug Finder analysis with the two options files: compile_opts created from your build command and run_opts created manually.
Polyspace Bug Finder™:
```
polyspace-bug-finder -options-file compile_opts -options-file run_opts
```
Polyspace Bug Finder Server™:
```
polyspace-bug-finder-server -options-file compile_opts -options-file run_opts
```
The analysis should complete without errors. You can open the results in the Polyspace user interface or upload the results to the Polyspace Access web interface (using the polyspace-access (Polyspace Access) command).
To run Code Prover instead of Bug Finder, use the polyspace-code-prover-server command instead of the polyspace-bug-finder-server command.

You can run a similar analysis using MATLAB scripts. Replace polyspace-bug-finder with the polyspaceBugFinder function and polyspace-configure with the function polyspaceConfigure.

Create Polyspace Analysis Configuration from Build Command (Makefile)

See Also

Related Topics