代码验证程序结果和源代码颜色

本主题介绍用于显示结果的各种颜色多空间®代码Prover™分析。

结果颜色

PolySpace通过特定的图标和颜色显示不同的验证结果成绩表和结果细节窗格。

运行时检查

多空间码验证器检查代码中的每个操作是否存在特定的运行时错误。软件会根据操作是否证明所有或某些执行路径上存在或不存在运行时错误来为操作指定颜色。

检查颜色 意图 实例 偶像

红色

突出显示在所有执行路径上导致特定错误的操作*.

多空间码验证器验证将参考语言标准确定错误。虽然某些错误对于特定编译环境可以接受，但它们违反了语言标准。要允许某些环境相关的行为，请使用适当的分析选项。有关更多信息，请参阅验证假设和检查行为.

红色溢出关于：

z=x+Y

操作+每一个值溢出x和Y核查在这一点上考虑的。
灰色

突出显示无法访问的代码。

灰色无法访问的代码检查：

如果（x>0）{}else{}

这个其他的分支对于所有值都无法访问x核查在这一点上考虑的。
橙色

突出显示可能在某些执行路径上导致错误的操作。

有关更多信息，请参阅橙色检查代码箴言.

橙色溢出关于：

z=x+Y

分析无法证明操作是否+溢出。

最常见的原因是，操作仅为某些值溢出x和Y核查在这一点上考虑的。您可以使用变量上的工具提示x和Y在操作中查看验证考虑的值范围。
绿色

突出显示经证明不会在所有执行路径上导致特定错误的操作*.

绿色溢出关于：

z=x+Y

操作+不会对的所有值溢出x和Y核查在这一点上考虑的。

*对于大多数检查，软件会在路径上的第一个运行时错误之后终止执行路径。因此，如果它证明某个操作存在明确错误（红色）或无错误（绿色），则该证明仅对代码中该点尚未终止的执行路径有效。请参阅在红色和橙色检查之后的代码抄本分析.

其他结果

除了检查运行时错误，多空间码验证器还显示有关代码的其他结果。

结果 意图 偶像
编码规则违规 表示违反预定义或自定义编码规则。 对于预定义规则和对于自定义规则。
代码度量 代码复杂性度量标准。 对于不超过指定限制的指标，以及对于超过限制的指标。
全局变量 表示全局变量声明。 对于共享可能未受保护的变量和对于非共享未使用的变量

源代码颜色

PolySpace使用以下颜色方案来显示代码来源窗格。

  • 支票行:

    每检查一次成绩表窗格，PolySpace将校验颜色分配给代码的相应部分。

    • 对于包含宏的行，如果宏已折叠，则Polyspace将使用该行上最严格检查的颜色对整个行进行着色。严重性按以下顺序降低：红色、灰色、橙色、绿色。

      这是遥不可及的对于循环包含一个宏最大尺寸. 整条线都是灰色的。

      如果没有签入包含宏的行，则当宏折叠时，Polyspace会在该行的下方加上黑色下划线。

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

      此任务有三个检查：我和used_global.被初始化但数组标签可以在其边界之外访问[操作员被涂成橙色以指示问题。

  • 与编码规则违规的行:

    对于每个编码规则违反成绩表窗格中，Polyspace指定给相应的关键字或标识符：

    • A.（倒三角形）符号，如果编码规则是预定义规则。可用的预定义规则是MISRA C®，臭臭®AC AGC、MISRA C++、JSF®C ++。

      这如果声明和||该行动违反了MISRA规则。

    • A.如果编码规则是自定义规则，则符号。

      此函数名违反自定义命名约定。

  • 带有工具提示的行:

    如果工具提示可用于关键字或标识符来源窗格，波尔多斯：

    • 如果关键字或标识符与支票关联，则对其使用实心下划线。

      该行上同时显示检查和工具提示输入,%和used_global..

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

      这一行上有工具提示对于和<，但没有检查它们。

    • 在函数调用或循环命令上使用虚线红色下划线，以指示函数正文或循环主体包含潜在的运行时错误。工具提示显示功能或循环主体中的行，导致错误。

      这个电话function_with_red.导致运行时错误。

  • 函数定义:

    当定义函数时，PolySpace颜色为蓝色中的函数名称。

  • 由于条件编译而停用的行:

    Polyspace为由于条件编译而停用的代码指定较浅的灰色阴影#ifdef未定义分支宏的语句。此代码不影响验证。

全局可变颜色

这个可变访问窗格显示代码中的全局变量以及对变量的读写操作。

例如，used_global.是一个全局变量，可访问四次：一次在初始化期间，一次在函数中function_with_red.，并在函数中执行两次function_with_grey..

配色方案如下：

  • 可变颜色:

    • 橙色：共享的、不受保护的全局变量（仅适用于多任务代码）

    • 绿色：共享，受保护的全局变量（仅适用于多任务代码）

    • 黑色：不共享，使用的全局变量

    • 灰色：未共享、未使用的全局变量

    看见全局变量.

  • 操作颜色：如果操作发生在无法访问的代码中，则为灰色，否则为黑色。

    在前面的示例中，函数中的一个操作function_with_grey.无法访问，但另一个是可以到达的。

有关更多信息，请参阅可变访问.

PolySpace代码箴言文档
万博1manbetx

试试MATLAB、Sim万博1manbetxulink和其他产品s manbetx 845

现在受审