解释 polyspace 桌面端用户界面中的 code prover 结果 -凯发k8网页登录

解释 polyspace 桌面端用户界面中的 code prover 结果

本主题展示了如何在 polyspace 桌面端产品的用户界面中审查 code prover 结果。若要了解如何在 polyspace access web 界面中审查结果，请参阅。

打开 polyspace^® code prover™ 分析的结果时，您会在结果列表窗格中看到一个列表。此列表包含运行时检查、编码违规、代码度量以及全局变量使用情况。

您可以首先缩小审查的重点：

使用结果列表列中的过滤器。例如，您可以先重点审查红色检查。
按文件和函数组织结果。请使用列表上方的图标。
由于 code prover 运行时检查的结果取决于前面检查的结果，因此审查从函数开始到结束的运行时检查很有帮助。

另请参阅。缩小列表范围后，您可以开始审查各个结果。本主题介绍了如何审查结果。

要开始审查，请在列表中选择一个结果。

解释结果

解释消息

第一步是了解问题所在。阅读结果详细信息窗格中的消息和源窗格中的相关代码行。

此时，您可能已经能够决定是否修复该问题。

消息由几个部分组成：

检查颜色和图标：请参阅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 运行时检查。离开当前结果后，可以使用结果详细信息窗格中的图标返回到该结果。

点击包含某个结果的源代码标记时，结果列表窗格中先前的结果选择以及结果详细信息窗格中的详细信息都将保持不变。您可以保持结果列表中的结果和结果详细信息固定的情况下，在源代码中导航。有时，您可能要查看与某个标记关联的结果。要更新结果选择和详细信息，请在按住 ctrl 键的同时点击该标记或右键点击并选择选择此位置处的相关结果。

在单独的窗口中导航

如果审查某个结果需要在源代码中进行更深入的导航，您可以创建一个重复的源代码窗口来关注该结果，在原始源代码窗口中导航。

右键点击源窗格并选择创建代码副本窗口。右键点击显示重复文件名（以 -spawn 1 结尾）的选项卡并选择新建垂直组。

在新建的重复文件窗口中执行导航步骤，同时缺陷仍然显示在原文件窗口中。调查完成后，关闭重复窗口。

解释 polyspace 桌面端用户界面中的 code prover 结果 -凯发k8网页登录