Code Prover 结果和源代码颜色

本主题解释了 Polyspace® Code Prover™ 分析结果的显示中使用的各种颜色。

结果颜色

Polyspace 会在结果列表和结果详细信息窗格中用特定图标和颜色显示不同验证结果。

Results list showing icons and colors for red checks, gray checks, orange checks, and green checks

运行时检查

Polyspace Code Prover 会检查代码中的每个运算中是否存在特定的运行时错误。该软件会根据是否已证实此运算在所有或某些执行路径上存不存在运行时错误，来指定相应的颜色。

检查颜色用途示例图标

红色

已证实运算在所有执行路径上都会导致特定错误。

Polyspace Code Prover 验证根据语言标准确定错误。可能有些错误在特定的编译环境中是可接受的，但它们违反了语言标准。要允许某些依赖于环境的行为，请使用适当的分析选项。有关详细信息，请参阅配置。

红色溢出检查：

z = x + y;

对于验证操作考虑的每个 x 和 y 值，+ 运算都会溢出。

Filled red circle
灰色

代码不可达。

灰色的不可达代码检查：

if(x > 0)
{}
else
{}

对于验证操作考虑的所有 x 值，else 分支都不可达。

Gray X
橙色

运算在某些执行路径上可能会导致错误。

有关详细信息，请参阅Orange Checks in Polyspace Code Prover。

橙色溢出检查：

z = x + y;

验证无法证实 + 运算是否会溢出。

最常见的原因是，只有对于验证操作考虑的某些 x 和 y 值，该运算才会溢出。您可以使用变量 x 和 y 上的工具提示来查看验证操作考虑的值范围。

Orange question mark
深橙色

已证实运算仅在某些执行路径上会导致特定错误。

当您使用敏感度上下文 (-context-sensitivity) 选项存储调用上下文信息，或使用内联 (-inline) 选项对每个函数调用进行内部克隆时，可能会出现深橙色检查。当您使用上述选项之一时，若运算在至少一条执行路径上为红色，并且在至少一条其他执行路径上为橙色或绿色，则会出现深橙色检查。

深橙色检查属于橙色检查的一种，您应优先审查，因为它们在某些上下文中可能包含确定的运行时错误。当您在审查工具条的聚焦过滤器部分中使用关键检查过滤器时，深橙色检查会显示在结果列表中。

深橙色除以零检查：

void func(int arg) {
    int loc_var = 0;
    loc_var = 1/arg;  
}

void main(void) {
    int num = 1;
    func(num + 10);
    func(num - 1);
}

/ 运算符显示为深橙色，这是因为在对 func 的多次调用中，第二次调用会引发除以零错误。

Dark orange question mark
绿色

已证实运算在所有执行路径上都不会导致特定错误。

绿色溢出检查：

z = x + y;

对于验证操作考虑的所有 x 和 y 值，+ 运算都不会溢出。

Green check mark

注意

在大多数检查中，一旦某条执行路径上出现运行时错误，该软件就会终止该路径。因此，如果它证实某个运算存在确定的错误（红色）或者没有错误（绿色），此证明仅对在代码的该点处尚未终止的执行路径有效。请参阅Code Prover Analysis Following Red and Orange Checks。

其他结果

除了针对运行时错误的检查外，Polyspace Code Prover 还会显示关于代码的其他结果。

结果用途图标
编码违规指示违反了预定义或自定义编码规则。Inverted purple triangle icon
代码度量指示代码复杂度度量。Blue star icon
全局变量指示全局变量声明。Blue X with orange question mark icon 表示潜在不受保护的共享变量，Blue X with gray X icon 表示未使用的非共享变量

源代码颜色

Polyspace 使用以下颜色方案在源代码窗格中显示代码。

  • 存在检查的行：

    对于结果列表窗格中的每项检查，Polyspace 都会为代码的对应部分指定检查颜色。

    • 对于包含宏的行，如果宏处于折叠状态，则 Polyspace 会将整个行显示为行中最严重检查的颜色。严重程度按以下顺序递减：红色、灰色、橙色、绿色。

      此不可达的 for 循环包含宏 MAX_SIZE。整个行的颜色为灰色。

      如果包含宏的行中没有检查，则当宏处于折叠状态时，Polyspace 会为该行显示黑色的下划线。

    • 对于所有其他行，Polyspace 仅会为与检查关联的关键字或标识符指定颜色。

      此赋值包含三项检查：i 和 used_global 已初始化，但数组 tab 可从其边界之外访问。[ 运算符显示为橙色即表示存在此问题。

  • 包含编码违规的行：

    对于结果列表窗格中的每个编码违规，Polyspace 都会为对应的关键字或标识符分配以下符号：

    • （倒三角形）符号（当编码规则为预定义规则时）。可用的预定义规则包括 MISRA C™、MISRA™ AC AGC、MISRA C++ 或 JSF® C++。

      以下示例中的 if 语句和 || 运算违反了 MISRA 规则。

    • 符号（当编码规则为自定义规则时）。

      以下示例中的函数名称违反了自定义命名约定。

  • 带有工具提示的行：

    如果源代码窗格中的某个关键字或标识符带有工具提示，则 Polyspace 会根据情况采取不同的措施：

    • 如果该关键字或标识符与检查相关联，则为其使用实线下划线。

      以下行中的 input、% 和 used_global 既存在检查，又带有工具提示。

    • 如果该关键字或标识符未与检查相关联，则对其使用虚线下划线。

      以下行中的 for 和 < 带有工具提示，但不存在针对它们的检查。

    • 对函数调用或循环命令使用红色的虚线下划线，来指示函数体或循环体包含潜在的运行时错误。工具提示会显示函数体或循环体中导致错误的行。

      以下对 function_with_red 的调用导致了运行时错误。

  • 函数定义：

    定义函数时，Polyspace 会以蓝色显示函数名称。

  • 由于条件编译而失效的代码行：

    Polyspace 会分配浅灰色给由于条件编译而被预处理排除的代码。例如，当 #ifdef 语句中某个分支的宏未定义时，将会出现这样的代码。此代码不会影响验证（或实际的运行时行为）。

全局变量颜色

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

可以使用结果详细信息窗格中的 Global Variables icon 图标，或转至视图 > 全局变量使用，来打开全局变量使用窗格。此外，您还可以在源代码窗格中选择一个全局变量，右键点击并选择显示全局变量使用情况，来打开全局变量使用窗格。

颜色方案如下所示：

  • 变量颜色：

    • 黑色：全局变量。

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

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

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

    请参阅全局变量。

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

有关详细信息，请参阅Polyspace 平台用户界面中的“全局变量使用”。

另请参阅

主题