Create Polyspace Platform Projects from Builds That Use Makefiles

You can create a Polyspace^® Platform project from a build command that builds your C/C++ sources and tests by using the polyspace-configure command.

The following is a simple example that illustrates how to create a pre-configured Polyspace Platform project from a makefile. This example uses the GCC compiler on the Linux^® platform, but you can adapt the makefile to other operating systems and compilers.

Example Files

Source and Test Files

Copy the folder polyspaceroot/polyspace/examples/doc_ps_setup/project_creation to a folder with write permissions. Here, polyspaceroot is the Polyspace installation folder.

Build System

Examine the makefile that compiles the source and test files, links the generated object files with a static library saturate.a, and produces an executable testRunner.

PSTUNIT_SOURCE = $(POLYSPACEROOT)/polyspace/pstest/pstunit/src/pstunit.c
PSTUNIT_INCLUDE = $(POLYSPACEROOT)/polyspace/pstest/pstunit/include

CC = gcc
CFLAGS = -O2 -Iinclude -I"$(PSTUNIT_INCLUDE)"
LDFLAGS = -Llib -l:saturate.a
OBJS = algo.o test.o pstunit.o

testRunner: $(OBJS)
	$(CC) $(OBJS) $(LDFLAGS) -o testRunner

algo.o: algo.c
	$(CC) -c algo.c $(CFLAGS)

test.o: test.c
	$(CC) -c test.c $(CFLAGS)

pstunit.o: $(PSTUNIT_SOURCE)
	$(CC) -c $(PSTUNIT_SOURCE) $(CFLAGS) -o pstunit.o

.PHONY: clean
clean:
	rm -f *.o testRunner

Check that the makefile builds the source and test files successfully. Open a command terminal, navigate to the folder (using cd) and enter:

make -B POLYSPACEROOT=polyspaceroot

Here, polyspaceroot is the Polyspace installation folder. 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 Platform project file.

The project_creation/include folder also contains a Windows^®-compatible version of the static library saturate.lib. To run this example on the Windows platform, in the makefile, change the definition of the LDFLAGS variable to LDFLAGS = -Llib -lsaturate.

Create Project for Static Analysis and Dynamic Testing

To create a workspace file myProject.psprjx for both static analysis and dynamic testing:

Trace your build system by running polyspace-configure:
```
polyspace-configure -output-platform-project myProject make -B POLYSPACEROOT=polyspaceroot
```
A project file myProject.psprjx is generated.
Open the project file in the Polyspace Platform User Interface.
The source file algo.c appears below the Code node of the project. The test file test.c appears below the Tests node of the project.
Double click the Configuration node of the project. On the Build tab of the Configuration pane:
- Compilation toolchain (Testing) is set to MINGW64 | gmake (64-bit Windows)
- Compilation toolchain (Static Analysis) is set to gnu x.x, depending on the GCC version
- Additional include paths is set to $(ROOTDIR)\include
- Extra C flags is set to -O2
- Library paths is set to $(ROOTDIR)\lib
- Libraries is set to saturate
See Information Gathered From Build Systems for Polyspace Analysis and Testing.

Sync Project with Updated Makefile

In your build system (makefile), if you update information about source and test files, include paths, or build configuration options, you can sync the myProject.psprjx file you created in the previous section by running this command:

polyspace-configure -update-platform-project myProject make -B POLYSPACEROOT=polyspaceroot

See Information Gathered From Build Systems for Polyspace Analysis and Testing.