Modularize Polyspace Analysis by Using Build Command

To configure a Polyspace^® analysis, you can reuse the compilation options in your build command such as make. First, you trace your build command with polyspace-configure (or polyspaceConfigure in MATLAB^®) and create a Polyspace options file. You later specify this options file for the subsequent Polyspace analysis.

If your build command creates several binaries, by default polyspace-configure groups the source files for all binaries into one Polyspace options file. If the same function occurs in multiple source files that are part of different binaries, lumping them into a single analysis can lead to link errors when you use the options file. In particular, you might see a link error because of multiple definitions of the main function.

This topic shows how to create a separate Polyspace options file for each binary created in your makefile. Suppose that a makefile creates four binaries: two executables (target cmd1 and cmd2) and two shared libraries (target liba and libb). You can create a separate Polyspace options file for each of these binaries.

Example Files

To try this example, use the files in polyspaceroot\polyspace\examples\doc_cxx\multiple_modules. Here, polyspaceroot is the Polyspace installation folder, for instance, C:\Program Files\Polyspace\R2024b or C:\Program Files\Polyspace Server\R2024b.

Build Source Code

Inspect the makefile. The makefile creates four binaries:

CC := gcc

LIBA_SOURCES := $(wildcard src/liba/*.c)
LIBB_SOURCES := $(wildcard src/libb/*.c)
CMD1_SOURCES := $(wildcard src/cmd1/*.c)
CMD2_SOURCES := $(wildcard src/cmd2/*.c)
LIBA_OBJ := $(notdir $(LIBA_SOURCES:.c=.o))
LIBB_OBJ := $(notdir $(LIBB_SOURCES:.c=.o))
CMD1_OBJ := $(notdir $(CMD1_SOURCES:.c=.o))
CMD2_OBJ := $(notdir $(CMD2_SOURCES:.c=.o))
LIBB_SOBJ := libb.so
LIBA_SOBJ := liba.so

all: cmd1 cmd2

cmd1: liba libb
	$(CC) -o  $@ $(CMD1_SOURCES) $(LIBA_SOBJ) $(LIBB_SOBJ)

cmd2: libb
	$(CC) -c $(CMD2_SOURCES) 
	$(CC) -o $@ $(CMD2_OBJ) $(LIBB_SOBJ)

liba: libb
	$(CC) -fPIC -c $(LIBA_SOURCES)
	$(CC) -shared -o $(LIBA_SOBJ) $(LIBA_OBJ) $(LIBB_SOBJ)

libb: 
	$(CC) -fPIC -c $(LIBB_SOURCES)
	$(CC) -shared -o $(LIBB_SOBJ) $(LIBB_OBJ) 

.PHONY: clean
clean: 
	rm *.o *.so

The binaries created have the dependencies shown in this figure. For instance, creation of the object cmd1.o depends on all .c files in the folder cmd1 and the shared objects liba.so and libb.so.

Build your source code by using the makefile. Use the -B flag to ensure full build.

make -B

Make sure that the build runs to completion.

Create One Polyspace Options File for Full Build

Trace the build command by using polyspace-configure. Use the option -output-options-file to create a Polyspace options file psoptions from the build command.

polyspace-configure -output-options-file psoptions make -B

Run Bug Finder or Code Prover by using the previously created options file: Save the analysis results in a results subfolder.

polyspace-bug-finder -options-file psoptions -results-dir results

polyspace-code-prover -options-file psoptions -results-dir results

You see this link error (warning in Bug Finder):

Procedure 'main' multiply defined.

The error occurs because the files cmd1/cmd1_main.c and cmd2/cmd2_main.c both have a main function. When you run your build command, the two files are used in separate targets in the makefile. However, polyspace-configure by default creates one options file for the full build. The Polyspace options file contains both source files resulting in conflicting definitions of the main function.

To verify the cause of the error, open the Polyspace options file psoptions. You see these lines that include the files with conflicting definitions of the main function.

-sources src/cmd1/cmd1_main.c
-sources src/cmd2/cmd2_main.c

Create Options File for Specific Binary in Build Command

To avoid the link error, build the source code for a specific binary when tracing your build command by using polyspace-configure.

For instance, build your source code for the binary cmd1.o. Specify the makefile target cmd1 for make, which creates this binary.

polyspace-configure -output-options-file psoptions -allow-overwrite make -B cmd1

Run Bug Finder or Code Prover by using the previously created options file.

polyspace-bug-finder -options-file psoptions -results-dir results

polyspace-code-prover -options-file psoptions -results-dir results

The link error does not occur and the analysis runs to completion. You can open the Polyspace options file psoptions and see that only the source files in the cmd1 subfolder and the files involved in creating the shared objects are included with the -sources option. The source files in the cmd2 subfolder, which are not involved in creating the binary cmd1.o, are not included in the Polyspace options file.

Special Considerations for Libraries (Code Prover only)

If you trace the creation of a shared object from libraries, the source files extracted do not contain a main function. In the subsequent Code Prover analysis, you can see an error because of the missing main.

Use the Polyspace option Verify module or library (-main-generator) (Polyspace Code Prover) to generate a main function. Specify the option in the options file that was created or directly at the command line. See Verify C Application Without main Function (Polyspace Code Prover).

In C++, use these additional options for classes:

Create One Options File Per Binary Created in Build Command

To create an options file for a specific binary created in the build command, you must know the details of your build command. If you are not familiar with the internal details of the build command, you can create a separate Polyspace options file for every binary created in the build command. The approach works for binaries that are executables, shared (dynamic) libraries and static libraries.

This approach works only if you use these linkers:

GNU^® — ld, gold, or ar linkers.
Visual C++^® — link.exe linker.

Trace the build command by using polyspace-configure.To create a separate options file for each binary, use the option -module with polyspace-configure.

polyspace-configure -module -output-options-path optionsFilesFolder make -B

The command creates options files in the folder optionsFilesFolder. In the preceding example, the command creates four options files for the four binaries:

cmd1.psopts
cmd2.psopts
liba_so.psopts
libb_so.psopts

You can run Polyspace on the code implementation of a specific binary by using the corresponding options file. For instance, you can run Code Prover on the code implementation of the binary created from the makefile target cmd1 by using this command:

polyspace-bug-finder -options-file optionsFilesFolder\cmd1.psopts -results-dir results

polyspace-code-prover -options-file optionsFilesFolder\cmd1.psopts -results-dir results

You can also loop through all the options files created using the -module option of polyspace-configure. For instance, the following Bash script runs Polyspace on all the generated options files, creating a separate results folder based on the options file name.

#!/bin/bash
FILEPATHS=optionsFilesFolder/*.psopts
for filePath in $FILEPATHS
do
    echo "Running Polyspace on $filePath"
    fileName="${filePath##*/}"
    resultsDirName="${fileName%.*}_results"
    logName="${fileName%.*}.log"
    polyspace-bug-finder -options-file "$filePath" -results-dir "${resultsDirName}" >> "${logName}"
done

#!/bin/bash
FILEPATHS=optionsFilesFolder/*.psopts
for filePath in $FILEPATHS
do
    echo "Running Polyspace on $filePath"
    fileName="${filePath##*/}"
    resultsDirName="${fileName%.*}"
    logName="{fileName%.*}.log"
    polyspace-code-prover -options-file "$filePath" -results-dir "${resultsDirName}" >> "${logName}"
done

For this approach, you do not need to know the details of your build command. However, 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 instance, the options file cmd1.psopts in this example specifies only the source files in the cmd1 subfolder and not the source files involved in creating the shared objects liba.so and libb.so. The subsequent analysis by using this options file cannot access functions from the shared objects and uses function stubs instead. In the Code Prover analysis, if you see too many orange checks due to the stubbing, use the approach stated in the section Create Options File for Specific Binary in Build Command.

Special Considerations for Libraries (Code Prover only)

In C++, use these additional options for classes: