主要内容

从使用联编文件的编译创建 Polyspace 平台工程

您可以通过使用 polyspace-configure 命令,从编译 C/C++ 源文件和测试文件的编译命令创建 Polyspace® 平台工程。

以下是一个简单示例,说明了如何从联编文件创建预配置的 Polyspace 平台工程。虽然此示例在 Linux® 平台上使用 GCC 编译器,但您可以调整联编文件以使用其他操作系统和编译器运行此示例。

示例文件

源文件和测试文件

polyspaceroot/polyspace/examples/doc_ps_setup/project_creation 文件夹复制到您有写入权限的文件夹。在这里,polyspaceroot 是 Polyspace 的安装文件夹。

编译系统

检查用于编译源文件和测试文件、将生成的对象文件与静态库 saturate.a 进行链接并生成可执行文件 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

检查联编文件是否成功编译了源文件和测试文件。打开命令行终端,导航到文件夹(使用 cd)并输入:

make -B POLYSPACEROOT=polyspaceroot
在这里,polyspaceroot 是 Polyspace 的安装文件夹。make 命令应完成执行且无错误。

-B 选项确保编译联编文件中的所有目标。通常,make 等编译命令被设置为仅编译自上次编译以来发生更改的源。但是,polyspace-configure 需要完整编译以确定将哪些源添加到 Polyspace 平台工程文件。

project_creation/include 文件夹中还包含静态库 saturate.lib 的 Windows® 兼容版本。要在 Windows 平台上运行此示例,请在联编文件中将 LDFLAGS 变量的定义更改为 LDFLAGS = -Llib -lsaturate

创建用于静态分析和动态测试的工程

要创建同时支持静态分析和动态测试的工作区文件 myProject.psprjx,请执行以下操作:

  1. 通过运行 polyspace-configure 跟踪您的编译系统:

    polyspace-configure -output-platform-project myProject make -B POLYSPACEROOT=polyspaceroot
    系统将生成工程文件 myProject.psprjx

  2. 在 Polyspace 平台用户界面中打开该工程文件。

  3. 源文件 algo.c 显示在工程的代码节点下方。测试文件 test.c 显示在工程的测试节点下方。

    双击工程的配置节点。在配置窗格的编译选项卡上:

    • 编译工具链(测试) 设置为 MINGW64 | gmake (64-bit Windows)

    • 编译工具链(静态分析) 设置为 gnu x.x,具体取决于 GCC 版本

    • 其他包含路径设置为 $(ROOTDIR)\include

    • 额外的 C 标志设置为 -O2

    • 库路径设置为 $(ROOTDIR)\lib

    • 设置为 saturate

    请参阅Information Gathered From Build Systems for Polyspace Analysis and Testing

将工程与更新后的联编文件同步

如果您在编译系统(联编文件)中更新了关于源文件和测试文件、包含路径或编译配置选项的信息,则可以通过运行以下命令同步在上一节中创建的 myProject.psprjx 文件:

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

请参阅Information Gathered From Build Systems for Polyspace Analysis and Testing

另请参阅

另请参阅

主题