在 Polyspace Access Web 界面中解释 Code Prover 结果
打开 Polyspace® Code Prover™ 分析的结果时,您会在结果列表窗格中看到一个列表。此列表包含运行时检查、编码违规、代码度量以及全局变量使用情况。
您可以首先缩小审查的重点:
使用工具条中的过滤器来缩小列表范围。例如,您可以重点关注影响程度高的缺陷。
点击结果列表中的某个列标题来根据该列的内容对列表进行排序。例如,您可以按组或按文件进行排序。
由于 Code Prover 运行时检查的结果取决于前面检查的结果,因此审查从函数开始到结束的运行时检查很有帮助。
另请参阅Filter and Sort Results in Polyspace Access Web Interface。缩小列表范围后,您可以开始审查各个结果。本主题介绍了如何审查结果。
要开始审查,请在列表中选择一个结果。
解释结果
解释消息
第一步是了解问题所在。阅读结果详细信息窗格中的消息和源代码窗格中的相关代码行。

消息由几个部分组成:
检查颜色和图标:请参阅Code Prover 结果和源代码颜色 (Polyspace Code Prover)。对于运行时错误检查:
:红色指示确定的错误。
:橙色指示可能的错误。
:灰色指示不可达代码。
:绿色指示不会发生特定错误。
运行时检查的描述。
在前面的示例中,检查会确定数组索引是否超出了数组边界。
与运行时检查相关的值。
在示例中,消息指出了数组大小 (127)、数组边界 (0..126) 以及数组索引变量在代码中的该点可以采用的值范围 (0..555)。
不精确检查的相关来源(对于橙色检查)。
在示例中,消息指出此检查可能是由两个易失变量导致的。
在源代码工具提示中查看变量范围
在源代码窗格中,带有工具提示的变量和运算显示有下划线。

在此示例中,以下项上显示有工具提示:
s8_ret:您可以看到它在+运算之前的数据类型和值范围。如果在 + 运算期间发生数据类型转换,则您还会在工具提示中看到此转换。
+:您可以看到左右操作数的值以及结果。=:您可以看到赋值期间发生的任何数据类型转换以及结果。
获取更多帮助
有时,您需要更多帮助才能得到一定的结果。要打开所选结果的帮助页面,请点击
图标。查看对结果进行说明的代码示例。
查明导致结果的根本原因
有时,根本原因可能与显示结果的实际位置相去甚远。例如,您读取的某个变量可能未初始化,因为初始化代码不可达。当您读取该变量时会显示该缺陷,但根本原因可能是前面的 if 或 while 条件始终为 false。
在源代码中导航
通常情况下,结果详细信息窗格会显示导致该结果的事件序列。不过,大多数情况下,您需要自己查找在代码中的导航路径。在浏览代码时根据变量上显示的工具提示跟踪变量范围的传播。
int func (int var) { /* Initial range of var */
…
var -= get (); /* New range of var */
…
set(&var); /* New range of var */
}
在用户界面中采用以下快速导航路径:
搜索对某个变量的所有引用并浏览它们。
在源代码窗格中右键点击变量名称,然后选择搜索所有引用。这些选项仅显示特定变量的实例,而不显示其他作用域中同名的其他变量。
从函数调用导航到其定义。
在源代码窗格中,右键点击函数名称。右键点击该函数并选择转至定义。
从函数导航到其调用方和被调用方。
点击结果详细信息窗格中的
图标。您可以看到包含该结果的函数,及其调用方和被调用方。点击调用方或被调用方名称可导航到调用点。双击某个名称可导航到定义。点击
图标可查看导致该结果的调用序列的图形表示。要导航到此序列中的函数,请点击图形中的节点。从函数调用或循环关键字导航到函数体或循环体中的某个错误。
如果该错误仅发生在某个特定的函数调用或特定的循环迭代中,则该函数调用或循环迭代会突出显示为红色。右键点击红色的函数调用或循环关键字。如果转至原因选项可用,请选择此选项。
在您开始在代码中的路径中进行导航之前,请确定您要查找的内容并选择合适的导航工具。例如:
要调查未初始化的变量缺陷,您可能需要确定该变量根本没有初始化。查找该变量的先前实例,并查看它是否已初始化。
要调查以下 MISRA C:2012 Rule 17.7 规则的违规情形:
您可能需要从函数调用导航到函数定义。The value returned by a function having non-void return type shall be used.
有关要查找的内容的其他示例,请参阅审查 Code Prover 运行时检查 (Polyspace Code Prover)。
如果您在源代码窗格中离开当前结果,点击结果详细信息窗格中的
图标可返回源代码窗格中该结果所在的位置。
点击包含某个结果的源代码标记时,结果列表窗格中先前的结果选择以及结果详细信息窗格中的详细信息都将保持不变。您可以保持结果列表中的结果和结果详细信息固定的情况下,在源代码中导航。有时,您可能要查看与某个标记关联的结果。要更新结果选择和详细信息,请在按住 Ctrl 键的同时点击该标记或右键点击并选择选择此位置处的相关结果。
存储源代码窗格导航和 Polyspace 操作
Polyspace 在导航历史记录窗格中显示某些审查工作流操作。
点击导航历史记录窗格中的一个操作,可在结果详细信息窗格中打开相关的结果。然后,在源代码窗格中导航到与该操作相关的代码位置。在继续审查结果的过程中,可以使用导航历史记录窗格返回之前的结果,并在源代码窗格中定位相关代码。
Polyspace 记录的操作包括:
在结果列表窗格中选择某个结果
从源代码窗格的右键点击菜单中选择保持在导航历史记录中的位置
在图中选择一个节点,例如错误调用图或变量访问图
在代码搜索、调用层次结构、全局变量使用或全局变量访问窗格中选择某一行
通过点击某个重要操作的行号,在导航历史记录窗格中对该操作进行标记。
点击
图标可从导航历史记录窗格中删除所有操作。
