Modularize Polyspace Projects by Using Makefile Builds

This topic shows how to create a separate Polyspace® project or options file for each binary created in your makefile. If your makefile creates several binaries, by default, when you create a project or options file from the makefile, the source files for all binaries are included in a single Polyspace project or options file. If the same function occurs in multiple source files that are part of different binaries, including them in a single build or analysis can lead to link errors when you use the project or options file.

Example Files

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

Build Source Code

Inspect the makefile below. The makefile creates four binaries: two executables (target cmd1 and cmd2) and two shared libraries (target liba and libb).

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 Project or Options File for Full Build

Trace the build command by using polyspace-configure and create one of the following:

  • Polyspace Platform project psproject.psprjx:

    polyspace-configure -output-platform-project psproject make -B

  • Options file psoptions for static analysis:

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

The newly created project or options file contains all sources that were compiled as part of the build.

Create Project or Options File for Specific Binary in Build Command

Instead of pooling all sources in a single project or options file, you can capture only the source files involved in creating a specific binary.

For instance, to capture the source files involved in creating the binary cmd1.o, build your source code for the binary by specifying the makefile target cmd1 for make. You can create one of the following:

  • Polyspace Platform project file:

    polyspace-configure -output-platform-project psproject -allow-overwrite make -B cmd1

  • Options file for static analysis:

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

Create One Project or 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 project or 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.

To create a separate options file for each binary, use the option -module with polyspace-configure. You can create one of the following:

  • A Polyspace Platform workspace with one project per binary in your build command:

    polyspace-configure -module -output-platform-project psWorkspace make -B

    The command creates a workspace file psWorkspace.pswks that contains four projects corresponding to the four binaries:

    • cmd1.psprjx

    • cmd2.psprjx

    • liba_so.psprjx

    • libb_so.psprjx

  • One Polyspace options file per binary in your build command:

    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

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.

See Also

Topics