从使用联编文件的编译创建 Polyspace 平台工程
您可以通过使用 polyspace-configure 命令,从编译 C/C++ 源文件和测试文件的编译命令创建 Polyspace® 平台工程。
以下是一个简单示例,说明了如何从联编文件创建预配置的 Polyspace 平台工程。虽然此示例在 Linux® 平台上使用 GCC 编译器,但您可以调整联编文件以使用其他操作系统和编译器运行此示例。
示例文件
源文件和测试文件
将 文件夹复制到您有写入权限的文件夹。在这里,polyspaceroot/polyspace/examples/doc_ps_setup/project_creation 是 Polyspace 的安装文件夹。polyspaceroot
编译系统
检查用于编译源文件和测试文件、将生成的对象文件与静态库 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,请执行以下操作:
通过运行
polyspace-configure跟踪您的编译系统:系统将生成工程文件polyspace-configure -output-platform-project myProject make -B POLYSPACEROOT=polyspaceroot
myProject.psprjx。在 Polyspace 平台用户界面中打开该工程文件。
源文件
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。