Main Content

Polyspace Access Web 界面中的全局变量

本主题主要介绍 Polyspace® Access Web 界面。要了解 Polyspace 桌面端用户界面中的等效窗格，请参阅Polyspace 桌面端用户界面中的变量访问 (Polyspace Code Prover)。

全局变量使用窗格会显示全局变量（和局部静态变量）。对于每个全局变量，此窗格会列出所有对变量执行读取/写入访问的函数和任务，以及它们的属性（例如值、读取/写入访问和共享使用）。

您可以使用结果详细信息窗格中的 图标，或转至窗 > 全局变量使用，来打开全局变量使用窗格。

The Global Variables pane lists all global variables along with attributes such as possible range of values, number of read and write operations, and so on.

对于每个变量和每项读取/写入访问，全局变量使用窗格都包含相关属性。围绕变量，下表中列出了各种属性。

属性描述
变量

变量的名称

值

变量的值（或值范围）

对于指针变量，此列为空。

读取次数变量被读取的次数
写入次数变量被写入的次数
由任务读取读取变量的任务数
由任务写入写入变量的任务数
保护

共享变量是否阻止并发访问

（仅当使用列的输入值为共享时才填写）

此列中可能的输入值为：

  • 临界区：如果变量在代码的临界区中被访问

  • 时序互斥：如果变量在互斥任务中被访问

有关这些输入值的详细信息，请参阅 Polyspace Code Prover™ 或 Polyspace Code Prover Server™ 文档。

使用如果变量是在任务之间共享的，则为 Shared；否则为空
文件包含变量声明的源文件
数据类型变量的数据类型（C/C++ 数据类型或结构体/类）

双击某个变量名称可在结果详细信息窗格中查看对该变量执行的读取/写入操作。结果详细信息窗格中的箭头符号 和 分别指示对全局变量执行读取和写入访问的函数。有关这些任务的更多信息，请参阅 Polyspace Code Prover 或 Polyspace Code Prover Server 文档中的分析选项 Tasks (-entry points)。

对于针对变量的访问操作，下表中列出了全局变量使用窗格中描述的各种属性。

属性描述
值

执行读取/写入访问的函数或任务中的变量的值或值范围

对于指针变量，此列为空。

由任务写入仅限任务：对变量执行写入访问的任务的名称
由任务读取仅限任务：对变量执行读取访问的任务的名称
文件包含对变量的访问操作的源文件

结果详细信息窗格还会列出对变量执行的访问操作的作用域。

例如，以全局变量 SHR2 为例：

The Result Details pane shows that the variable SHR2 is shared among several tasks and some of the operations on SHR2 are not protected against concurrent access. The Result Details pane also shows the possibly conflicting operations.

文件 tasks1.c 中的函数 Tserver 对 SHR2 执行两个写入操作。在结果详细信息窗格中，这由表中标有 的两个 Tserver() 实例予以指示。类似地，任务 initregulate 的读取访问也列在表中并标有 。

全局变量使用窗格中用于变量的颜色方案为：

  • 黑色：全局变量。

  • 橙色：在任务之间共享的且不阻止并发访问的全局变量。

  • 绿色：在任务之间共享的且阻止并发访问的全局变量。

  • 灰色：已声明但在可达代码中未使用的全局变量。

如果某个任务对全局变量执行某些操作，但这些操作在不可达代码中，则该任务将被着色为灰色。

从全局变量使用窗格中获取的有关全局变量和读取/写入访问操作的信息称为数据字典。

您还可以从全局变量使用窗格执行以下操作。

  •  查看结构化变量

  •  显示/隐藏调用方和被调用方

  •  隐藏不可达代码中的访问

  •  限制