Polyspace Bug Finder 与 Polyspace Code Prover 之间的差别
Polyspace® Bug Finder™ 和 Polyspace Code Prover™ 都通过静态分析检测运行时错误。尽管这两款产品的用户界面相似，用于分析的底层数学运算有时可能也相同，但这两款产品的目标不同。
Bug Finder（或 Polyspace as You Code，它与 Bug Finder 相似，但执行单文件分析）可快速分析您的代码并检测多种类型的缺陷。Code Prover 检查您的代码中的每个运算是否存在一组可能的运行时错误，并尝试证明所有执行路径都不存在错误。
注意
对于代码中的每个运算，Code Prover 会考虑所有通向该运算且之前未发生过错误的执行路径。如果执行路径在运算前包含错误，那么 Code Prover 不会考虑该路径。请参阅Code Prover Analysis Following Red and Orange Checks。
例如，对于您的代码中的每个除法，Code Prover 分析都会尝试证明分母不能为零。Bug Finder 不会执行这种详尽验证。例如，Bug Finder 也会检查除以零错误，但它可能无法找出导致该错误的所有运算。
由于在目标方面存在上述差别，因此，这两种产品在设置、分析和结果审查方面都有差别。下述内容将重点介绍 Bug Finder 与 Code Prover 分析（也称为验证）之间的主要差别。根据您的需求，您可以在软件开发生命周期的适当时间点采用其中一种或同时采用两种分析。
Bug Finder 和 Code Prover 之间的差异概述
在开发过程中会定期同时用到 Bug Finder 和 Code Prover。这两款产品提供的功能各不相同，但彼此互补。有关同时使用这两款产品的可能方式，请参阅同时使用 Polyspace Bug Finder 和 Polyspace Code Prover 的工作流。
下表概述了这两款产品如何互补。有关详细信息，请参阅下面各部分的内容。
| 功能 | Bug Finder | Code Prover |
|---|---|---|
| 检查项的数量 | 有 300 多个用于检测缺陷的检查项 | 针对重大运行时错误执行 30 项检查，针对全局变量用法执行 4 项检查 |
| 分析深度 | 快速。 例如：
| 详尽。 例如：
|
| 报告准则 | 可能的缺陷 | 经过证明的检查结果 |
| Bug 调查结果准则 | 很少误报 | 零漏报 |
Bug Finder 和 Code Prover 如何互补
使用 Bug Finder 更快地进行分析
Bug Finder 分析速度的快慢取决于应用程序的大小。Bug Finder 分析时长随应用程序的大小呈线性增长。Code Prover 验证时长的增长速度快于线性。
一种可能的工作流是运行 Code Prover 来分析模块或库在出现某些错误时的鲁棒性，并在集成阶段运行 Bug Finder。对大型代码库执行的 Bug Finder 分析可以在更短的时间内完成，并且还会发现诸如声明不匹配和数据争用的集成缺陷。
使用 Code Prover 可以进行更详尽的验证
Code Prover 尝试证明以下情况：
每个除法或模数运算不存在除以零错误
每个数组访问不存在数组索引越界错误
每个变量读取不存在未初始化的变量错误
每个可能会溢出的运算不存在 错误
并且不存在诸如此类的其他错误。
对于每个运算：
如果 Code Prover 可以证明所有执行路径都不存在错误，则它会以绿色突出显示该运算。
如果 Code Prover 可以证明针对所有执行路径存在某个确定的错误，则它会以红色突出显示该运算。
如果 Code Prover 无法证明不存在错误，也无法证明存在某个确定的错误，则它会以橙色突出显示该运算。这一小部分的橙色检查意味着您必须通过目视检查或测试仔细审查这些运算。橙色检查通常表示隐藏的漏洞。例如，该运算在当前上下文中可能是安全的，但在另一个上下文中重用时可能会失败。
您可以使用 Polyspace 用户界面中提供的信息来诊断检查。请参阅使用 Code Prover 时数据和控制流分析更严格。您还可以提供上下文信息以进一步减少未经证明的代码，例如，从外部约束输入范围。
Bug Finder 的目标不是进行详尽的分析。它努力检测出尽可能多的 Bug 并减少误报。对于关键的软件组件，仅仅运行 Bug 查找工具是不够的，因为即使修复了分析中发现的所有缺陷，但在代码执行过程中仍然可能会出现错误（漏报）。对代码运行 Code Prover 并解决发现的错误后，预计代码的质量会更高。请参阅Code Prover 旨在实现零漏报。
使用 Bug Finder 可以检测更具体的缺陷类型
Code Prover 会针对各种运行时错误在可能存在错误的地方进行检查，用数学方法证明不存在该错误。除了检测可以用数学方法证明其不存在的错误之外，Bug Finder 还会检测其他缺陷。
例如，根据 C 语言标准，语句 if(a=b) 语义正确，但该语句经常会导致意外的赋值。Bug Finder 会检测这类意外的运算。尽管 Code Prover 不检测这类意外的运算，但它可以检测意外的运算是否导致其他运行时错误。
Bug Finder 会检测但 Code Prover 不会检测的缺陷示例包括良好做法缺陷、资源管理缺陷、某些编程缺陷、安全缺陷，以及 C++ 面向对象的设计中的缺陷。
有关详细信息，请参阅：
使用 Bug Finder 的设置过程更简单
即使您的代码在您的编译工具链中成功编译，它在 Code Prover 验证的编译阶段也可能会失败。Code Prover 中的严格编译关系到它是否有能力证明某些运行时错误不存在。
Code Prover 严格遵循 ANSI® C99 标准，除非您显式使用模仿您的编译器的分析选项。
要允许偏离 ANSI C99 标准，必须使用目标和编译器选项。如果您通过您的编译系统创建 Polyspace 工程，则会自动设置这些选项。
Code Prover 不允许常见编译器可能允许的链接错误。
虽然您的编译器允许链接错误（例如编译单元之间的函数签名不匹配），但为了避免在运行时出现意外行为，必须修复这些错误。
有关详细信息，请参阅Troubleshoot Compilation and Linking Errors。
Bug Finder 对某些编译错误没有那么严格。链接错误（例如不同编译单元之间的函数签名不匹配）可能会阻止 Code Prover 验证，但不会阻止 Bug Finder 分析。因此，只需执行较少的设置工作便可运行 Bug Finder 分析。在 Bug Finder 中，分析完成后，链接错误通常被报告为缺陷。
使用 Bug Finder 时运行较少次数便可得到干净的代码
为了保证不存在某些运行时错误，Code Prover 在运算中检测到运行时错误后会遵守严格的规则。一旦发生运行时错误，程序的状态将变为未明确定义，并且 Code Prover 无法证明后续代码中不存在错误。因此：
如果 Code Prover 证明存在确定的错误并将检查显示为红色，则它不会验证同一代码块中的其余代码。
例外包括溢出等检查，如果出现这样的例外，分析将继续，而溢出结果将被截断或换行。
如果 Code Prover 怀疑存在错误并将检查显示为橙色，则它不会考虑包含错误的路径。例如，如果 Code Prover 在运算
1/x中检测到除以零错误，则在该代码块中有关x的后续运算中，x不能为零。如果 Code Prover 检测到某个代码块无法访问并且检查显示为灰色，则它不会检测该代码块中的错误。
有关详细信息，请参阅Code Prover Analysis Following Red and Orange Checks。
因此，在修复红色和灰色检查项并重新运行验证后，您可能会发现更多问题。您需要多次运行验证并修复每次发现的问题，才能得到完全干净的代码。这种情况类似于动态测试。在动态测试中，修复代码中某个位置的错误后，您可能会在后续代码中发现新的错误。
Bug Finder 在某个代码块中发现缺陷后不会停止该代码块中的整个分析。即使是使用 Bug Finder，您可能也必须多次运行分析才能获得完全干净的代码。但是，所需的运行次数会少于 Code Prover。
使用 Bug Finder 会实时显示结果
Bug Finder 在分析仍在运行时就会显示一些分析结果。您不必等待分析结束便可审查这些结果。
Code Prover 只有在验证结束后才会显示结果。一旦 Bug Finder 发现某个缺陷，便可显示该缺陷。Code Prover 必须证明在所有执行路径上都不存在错误。因此，它无法在分析期间显示结果。
使用 Code Prover 时数据和控制流分析更严格
对于代码中的每个运算，Code Prover 会提供：
工具提示，显示运算中每个变量的值范围。
对于指针，工具提示会显示指针指向的变量以及变量值。
可引发运算的函数调用序列的图形表示形式。
通过使用此范围信息和调用图，您可以轻松在函数调用层次结构中导航，并了解变量如何获取导致错误的值。例如，对于数组索引越界错误，您可以发现索引变量最先被赋予导致错误的值的位置。
在 Bug Finder 中审查结果时，您还会看到支持信息来帮助您了解缺陷根源。例如，您可以从 Bug Finder 发现缺陷的位置回溯到其根本原因。不过，在 Code Prover 中，您可以得到更完整的信息，这些信息可以帮助您了解代码中的所有执行路径。
Code Prover 中的数据流分析
Code Prover 中的控制流分析
Bug Finder 误报很少
Bug Finder 旨在尽量减少误报，也就是尽量减少报告您不太可能修复的结果。默认情况下，只会显示对您最有意义的缺陷。
Bug Finder 还会根据缺陷的严重性和误报率，为缺陷类型指定一个名为 impact 的属性。您可以选择仅针对高影响缺陷来分析代码。您还可以启用或禁用您不想审查的缺陷。
您还可以禁用某些与非初始化相关的 Code Prover 缺陷。
Code Prover 旨在实现零漏报
Code Prover 旨在进行详尽的分析。该软件会检查可能触发特定类型的错误的每个运算。如果某个代码运算显示为绿色，则意味着该运算不会导致出现软件所检查的那些运行时错误。该软件旨在通过这种方式实现零漏报。
仅当在与通过分析选项提供给 Code Prover 的相同条件下执行代码时，Code Prover 结果才有效。
如果该软件无法证明不存在错误，则它会以红色或橙色突出显示可疑运算，并要求您审查该运算。
Bug Finder 中支持的编码规则
Bug Finder 支持检查是否符合外部编码标准，例如：
AUTOSAR C++14。请参阅 AUTOSAR C++14 规则。
MISRA C:2012。请参阅 MISRA C:2012 指令和规则。
MISRA C++:2008。请参阅 MISRA C++:2008 规则。
CERT C。请参阅 CERT C 规则和建议。
CERT C++。请参阅 CERT C++ 规则。
有关支持的编码标准的完整列表，请参阅 Polyspace 编码规范支持。
