通过联编文件编译对 Polyspace 工程进行模块化处理

本主题介绍如何为在联编文件中创建的每个二进制文件创建单独的 Polyspace® 工程或选项文件。如果您的联编文件创建了多个二进制文件，则默认情况下，当您从该联编文件创建工程或选项文件时，所有二进制文件对应的源文件都会包含在单个 Polyspace 工程或选项文件中。如果同一个函数出现在多个属于不同二进制文件的源文件中，若将它们放在单个编译或分析中，在使用该工程或选项文件时可能会导致链接错误。

示例文件

要尝试此示例，请使用 polyspaceroot\polyspace\examples\doc_ps_setup\multiple_modules 中的文件。其中，polyspaceroot 是 Polyspace 的安装文件夹，例如 C:\Program Files\Polyspace\R2026a 或 C:\Program Files\Polyspace Server\R2026a。

编译源代码

检查下方的联编文件。该联编文件创建了四个二进制文件：两个可执行文件（目标 cmd1 和 cmd2）以及两个共享库（目标 liba 和 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

创建的二进制文件具有下图所示的依赖关系。例如，cmd1.o 对象的创建依赖于 cmd1 文件夹中的所有 .c 文件以及共享对象 liba.so 和 libb.so。

使用该联编文件编译您的源代码。使用 -B 标志以确保完整编译。

make -B

确保编译运行至完成。

为完整编译创建单个工程或选项文件

使用 polyspace-configure 跟踪编译命令，并创建以下项之一：

  • Polyspace 平台工程 psproject.psprjx：

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

  • 用于静态分析的选项文件 psoptions：

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

新创建的工程或选项文件包含在编译过程中编译的所有源文件。

为编译命令中的特定二进制文件创建工程或选项文件

您可以只捕获创建特定二进制文件所涉及的源文件，而不是将所有源文件归入单个工程或选项文件。

例如，要捕获创建二进制文件 cmd1.o 所涉及的源文件，请通过为 make 指定联编文件目标 cmd1 来编译该二进制文件对应的源代码。您可以创建以下项之一：

  • Polyspace 平台工程文件：

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

  • 用于静态分析的选项文件：

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

为编译命令中创建的每个二进制文件创建一个工程或选项文件

要为编译命令中创建的特定二进制文件创建选项文件，您必须了解编译命令的详细信息。如果您不熟悉编译命令的内部细节，可以为编译命令中创建的每个二进制文件创建单独的 Polyspace 工程或选项文件。此方法适用于可执行文件、共享（动态）库和静态库类型的二进制文件。

此方法仅在您使用以下链接器时有效：

  • GNU® - ld、gold 或 ar 链接器。

  • Visual C++® - link.exe 链接器。

要为每个二进制文件创建单独的选项文件，请在 polyspace-configure 中使用 -module 选项。您可以创建以下项之一：

  • Polyspace 平台工作区，其中为编译命令中的每个二进制文件创建一个工程：

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

    该命令会创建一个工作区文件 psWorkspace.pswks，其中包含与四个二进制文件对应的四个工程：

    • cmd1.psprjx

    • cmd2.psprjx

    • liba_so.psprjx

    • libb_so.psprjx

  • 为编译命令中的每个二进制文件创建一个 Polyspace 选项文件：

    polyspace-configure -module -output-options-path optionsFilesFolder make -B

    该命令会在文件夹 optionsFilesFolder 中创建选项文件。在前面的示例中，该命令为四个二进制文件创建了四个选项文件：

    • cmd1.psopts

    • cmd2.psopts

    • liba_so.psopts

    • libb_so.psopts

使用此方法时，您不需要了解编译命令的详细信息。但是，当您以这种方式为每个二进制文件创建单独的选项文件时，每个选项文件只包含直接参与该二进制文件的源文件，不包含通过共享对象引入的源文件。例如，此示例中的选项文件 cmd1.psopts 仅指定 cmd1 子文件夹中的源文件，不指定创建共享对象 liba.so 和 libb.so 所涉及的源文件。后续使用此选项文件执行的分析将无法访问来自共享对象的函数，而是使用函数桩件代替。

另请参阅

主题