修复与 TASKING 编译器相关的 Polyspace 编译错误

如果您为编译工具链(静态分析) 选项选择 tasking，则可能会遇到此问题。

问题

在 Polyspace® 分析过程中，您会看到与特定于 Tasking 编译器的扩展相关的错误，例如与特殊函数寄存器数据类型相关的错误。

解决方案

启用对 SFR 类型的支持

在使用 TASKING 编译器进行编译时，通常需要使用以下编译器标志来指定特殊函数寄存器 (SFR) 数据类型的声明位置：

  • --cpu=xxx:编译器会在您的源文件中以 #include 命令隐式包含文件 sfr/regxxx.sfr。在以 #include 命令包含该文件后，您可以使用在该 .sfr 文件中声明的特殊函数寄存器 (SFR)。

  • --alternative-sfr-file:编译器使用替代 SFR 文件而不是常规 SFR 文件。您可以使用在该替代 SFR 文件中声明的特殊函数寄存器 (SFR)。

如果您为 Polyspace 分析指定了 TASKING 编译器，则该分析会对这些编译器标志做出如下假设：

  • --cpu=xxx:此分析会选择一个特定值 xxx。如果您为 TASKING 编译器使用不同的值，则在 Polyspace 分析过程中可能会遇到错误。

    Polyspace 分析使用的 xxx 值取决于您选择的目标处理器类型 (-target)：

    • tricore：tc1793b

    • c166：xc167ci

    • rh850：r7f701603

    • arm：ARMv7M

  • --alternative-sfr-file:此分析假设您不使用替代 SFR 文件。如果您使用替代 SFR 文件，则会遇到错误。

如下所示在 Polyspace 分析中使用命令行选项 -compiler-parameter。您可使用此命令行选项来让 Polyspace 识别您的编译器标志。在用户界面中，您可以在其他字段中输入此命令行选项。您可以多次输入此选项。

  • --cpu=xxx:对于您的 Polyspace 分析，请使用

    -compiler-parameter --cpu=xxx
    其中，xxx 是您在使用编译器进行编译时所使用的值。

  • --alternative-sfr-file:对于您的 Polyspace 分析，请使用

    -compiler-parameter --alternative-sfr-file

    如果您仍然因为 Polyspace 找不到您的 .asfr 文件而遇到错误，请使用选项 Include (-include) 在预处理代码中以 #include 命令显式包含您的 .asfr 文件。

    通常，该文件的路径为 Tasking_C166_INSTALL_DIR\include\sfr\regCPUNAME.asfr。例如，如果 TASKING 编译器安装在 C:\Program Files\Tasking\C166-VX_v4.0r1\，并且您使用与 CPU 相关的标志 -Cxc2287m_104f 或 --cpu=xc2287m_104f，则路径为 C:\Program Files\Tasking\C166-VX_v4.0r1\include\sfr\regxc2287m.asfr。

    当您跟踪编译命令时，如果使用了替代 SFR 文件，也可能会遇到相同的问题。有关详细信息，请参阅从编译系统创建 Polyspace 工程的要求。

启用对 TC1793 之外的 CPU 的支持

如果您为编译工具链(静态分析) 选项选择 tasking，则使用的 CPU 为 TC1793。如果您使用的是其他 CPU，请在您的工程中设置以下分析选项：

如果您不是手动指定编译器，而是跟踪您的编译命令 (makefile)，则 Polyspace 可以检测您的 CPU 并在工程中添加所需的定义。

避免使用不支持的构造

Polyspace 不支持某些特定于 TASKING 编译器的构造。

有关不支持的构造的列表，请参阅 polyspaceroot\polyspace\verifier\code_prover_desktop 中的 codeprover_limitations.pdf。其中，polyspaceroot 是 Polyspace 的安装文件夹，例如 C:\Program Files\Polyspace\R2019a。