审查 Polyspace Code Prover 分析结果

示例文件

要遵循本教程中的步骤，请使用在桌面端运行 Polyspace Code Prover中的步骤运行 Polyspace。或者，在 Polyspace 用户界面中，使用帮助 > 示例 > Bug_Finder_Example.psprj 打开示例结果。如果您在上传示例结果后进行了一些更改，要加载最新副本，请选择帮助 > 示例 > 还原默认示例。

解释结果

审查每个 Polyspace 结果。查找问题的根本原因。

请从结果列表窗格中的结果列表开始。

要按照结果的严重程度进行排序，请点击族别列标题。在 example.c 文件中选择红色非法解引用指针检查。红色检查表示错误发生在分析中涉及的所有执行路径上。

在源窗格中查看源代码，并在结果详细信息窗格中查看有关结果的更多信息。

对于非法解引用指针结果，结果详细信息窗格中的消息指示指针 p 具有 400 字节的可用缓冲区。它指向从缓冲区开头 400 字节处开始的位置，并指向 4 字节的数据类型。

要进一步调查并找出问题的根本原因，请右键点击源窗格中的变量 p 并选择搜索所有引用。点击每个搜索结果可导航到源代码中的对应位置。在每个位置，将光标放在变量 p 上可查看描述代码中该点变量值的工具提示。

您会看到指针变量 p 被初始化为一个包含 100 个元素的 int 数组。指针以 for 循环遍历数组 100 次，然后指向数组的末尾。在红色非法解引用指针检查所在的行上，此指针进行了解引用，导致对数组外的某个内存位置解引用。

通过 Bug 修复或注释来处理结果

在了解某个 Polyspace 检查结果的根本原因后，您可以修复代码。或者，为 Polyspace 结果添加注释，以便日后修复代码或者对结果进行申述。可以使用注释来跟踪审查进度。

在源窗格中，右键点击变量 p。选择打开编辑器。代码将在文本编辑器中打开。修复问题。例如，您可以让指针在 for 循环之后指向数组的开头。下面高亮显示了对代码的更改。

...
int i, *p = array;

for (i = 0; i < 100; i++) {
    *p = 0;
     p++;
}

p = array;

if (get_bus_status() > 0)
...

另外，如果您不希望立即修复缺陷，请为结果指定待调查状态。还可以添加注释以进一步进行解释。

如果您指定未计划任何操作状态，则同一工程上的后续运行中便不会再出现该结果。

管理结果

打开 Code Prover 分析的结果时，您会看到包含运行时检查、编码违规或其他结果的列表。为了便于审查，您可以缩小列表范围，或者按文件或结果类型对结果进行分组。

例如，您可以：