用于桌面端和服务器端的 Polyspace 产品
Polyspace Bug Finder
Polyspace® Bug Finder™ 可标识 C 和 C++ 嵌入式软件中的运行时错误、并发性问题、安全漏洞和其他缺陷。Polyspace Bug Finder 使用静态分析（包括语义分析）来分析软件控制、数据流和过程间行为。通过在检测到缺陷后立即突出显示缺陷，您可以在开发过程的早期对 Bug 进行分类和修复。
Polyspace Bug Finder 可检查您的代码是否符合编码规则标准，例如 MISRA C™、MISRA C++、JSF++、CERT® C、CERT C++ 以及自定义命名约定。它将生成报告，其中包含发现的 Bug、代码违规，以及代码质量度量（包括圈复杂度）。Polyspace Bug Finder 可以与 Eclipse™ IDE 配合使用以在桌面端分析代码。
对于自动生成的代码，可以从 Polyspace 结果追溯到 Simulink® 模型和 dSPACE® TargetLink® 模块。
通过 IEC Certification Kit (for ISO 26262 and IEC 61508) 和 DO Qualification Kit (for DO-178) 实现对行业标准的支持。
对于特定于桌面端的工作流，请参阅：
在桌面端安装 Polyspace 产品 (R2025b) (Polyspace Bug Finder)
在桌面端设置 Bug Finder 分析 (R2025b) (Polyspace Bug Finder)
审查 Polyspace Bug Finder 结果 (R2025b) (Polyspace Bug Finder)
Polyspace Code Prover
Polyspace Code Prover™：是一个可靠的静态分析工具，可证明 C 和 C++ 源代码中不存在溢出、除以零、数组访问越界和其他运行时错误。它无需程序执行、代码插桩或测试用例即可生成结果。Polyspace Code Prover 使用基于形式化方法的语义分析和抽象解释来验证软件的过程间行为、控制行为和数据流行为。您可以用它来验证手写代码、生成的代码或这两者的组合。每个代码语句都进行了着色，以指示它是否存在运行时错误、是否已证明失败、是否不可达或是否未经证明。
Polyspace Code Prover 会显示变量和函数返回值的范围信息，并且可以证明哪些变量超出了指定的范围限制。代码验证结果可用于跟踪质量度量并检查是否符合您的软件质量目标。Polyspace Code Prover 可与 Eclipse IDE 配合使用以验证桌面端代码。
通过 IEC Certification Kit (for IEC 61508 and ISO 26262) 和 DO Qualification Kit (for DO-178)实现对行业标准的支持。
对于特定于桌面端的工作流，请参阅：
在桌面端安装 Code Prover (R2025b) (Polyspace Code Prover)
在桌面端设置 Code Prover 分析 (R2025b) (Polyspace Code Prover
在 Polyspace 用户界面中审查 Polyspace Code Prover 结果 (R2025b) (Polyspace Code Prover)
