Main Content

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)实现对行业标准的支持。

Polyspace Code Prover 快速入门

Polyspace Code Prover 基础知识学习

安装 Polyspace

在桌面端或服务器端安装 Polyspace 产品进行分析

配置并运行分析

在桌面端或服务器端设置 Polyspace Code Prover 分析

审查分析结果

在 Polyspace 桌面端用户界面或 Web 浏览器中审查 Polyspace Code Prover 结果

Polyspace Code Prover 示例

用于从不同环境运行 PolyspaceCode Prover 的示例脚本和模板,显示运行时错误的 C/C++ 代码示例

工具鉴定与认证

针对 DO 和 IEC 认证对 Polyspace Code Prover 进行鉴定

Polyspace Code Prover 中的故障排除

解决 Polyspace Code Prover 中的意外问题