Polyspace Access Web 界面中的全局变量

R2026b

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

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

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 的读取访问也列在表中并标有。

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

黑色：全局变量。
橙色：在任务之间共享的且不阻止并发访问的全局变量。
绿色：在任务之间共享的且阻止并发访问的全局变量。
灰色：已声明但在可达代码中未使用的全局变量。

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

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

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

对于结构化变量，双击全局变量使用窗格中的变量以查看各个字段。例如，对于结构体 SHR4，该窗格会显示字段 SHR4.A 和 SHR4.B，以及对它们执行读取/写入访问的函数。
自定义全局变量使用窗格以仅显示共享变量。在全局变量使用窗格工具栏上，点击“非共享变量”按钮以显示或隐藏非共享变量。
通过点击过滤器按钮可隐藏出现在不可达代码中的读取/写入访问。

限制

在全局变量使用窗格中，对全局变量或对象（在 C++ 中）的寻址操作不会显示为读取/写入操作。以如下 C++ 代码为例：

class C0 
{ 
public: 
  C0() {} 
  int get_flag() 
  { 
    volatile int rd; 
    return rd; 
  } 
  ~C0() {} 
private: 
  int a;                /* Never read/written */ 
}; 

C0 c0;                  /* c0 is unreachable */ 

int main() 
{ 
  if (c0.get_flag())    /* Uses address of the method */ 
    { 
      int *ptr = take_addr_of_x(); 
      return 1; 
    } 
  else 
    return 0; 
}

您在全局变量使用窗格中不会看到方法调用 c0.get_flag()，因为该调用是对属于对象 c0 的方法的寻址操作。