Examples 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

In the example folder, you will find a makefile that creates four binaries:

Inspect the makefile:

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 Single Project From Build Command

First create a single Polyspace Platform project from the above build command and run static analysis using the project.

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 places all source files in the same project, resulting in multiple definitions of the main() function.

Create Project From 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-platform-project psProjectCmd1 -allow-overwrite make -B cmd1

When you run Bug Finder or Code Prover on the resulting project or try to build the project, the link error does not occur and the run completes successfully. You can see that the project contains only the source files in the cmd1 subfolder and the files involved in creating the shared objects. The source files in the cmd2 subfolder, which are not involved in creating the binary cmd1.o, are not included in the Polyspace project.

Create One Project Per Binary 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.

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-platform-project psWorkspace make -B

The command creates a Polyspace Platform workspace psWorkspace.pswks with four projects corresponding to the four binaries:

You can run Bug Finder or Code Prover on any of the projects without running into issues because of multiple definition of the main() function.