Polyspace Code Prover

证明软件中不存在运行时错误

Polyspace Code Prover 可以证明在 C 和 C++ 源代码中不存在溢出、除以零、数组访问越界和特定的其他运行时错误。它不需要执行程序、代码插桩或测试用例即可产生结果。Polyspace Code Prover 使用基于形式化方法的静态分析和抽象解释。您可以用它来验证手写代码、生成的代码或两者的组合。每个操作都采用着色表明是否无运行时错误、证明有缺陷、不可达或未经证明。

Polyspace Code Prover 还显示变量和函数返回值的范围信息，并且可以证明哪些变量超出指定范围限制。结果可以发布到控制板上，以跟踪质量指标并确保符合软件质量目标。

通过 IEC Certification Kit (for IEC 61508 and ISO 26262) 和 DO Qualification Kit (for DO-178)，可提供对行业标准的支持。

证明不存在严重的运行时错误

根据所有可能的输入，在不执行代码的情况下分析所有代码路径。识别无论运行时条件如何都永远不会遇到运行时错误的语句，并找出其他需要注意的语句。

文档

改进软件设计和代码理解

检查 C/C++ 代码中的控制流和数据流，查看与变量和运算符相关联的范围信息。

文档

优化软件性能

通过识别安全可靠的运算（如除以零和溢出）来删除防御性代码。检测无法通过任何执行路径到达的代码分支。找出逻辑和程序结构中的错误，删除它们以减少内存占用。

文档

分析全局变量用法

减少调试全局变量（包括任务或线程共享的变量）的读/写操作所花费的时间。
使用并发访问图了解可能导致数据竞争问题的控制流和数据流。识别未使用的全局变量以进行代码优化。

文档

认证支持

创建完成行业标准认证过程所需的交付物。经 TÜV 南德认证，符合 IEC 61508 和 ISO 26262 标准。使用为 DO-178C 流程准备的报告和交付物。

文档

Simulink 和 Stateflow 集成

对生成的代码运行分析，并将您的发现追溯到源 Simulink 模型模块和 Stateflow 图。从 Simulink 环境中启动 Polyspace^® 分析。

文档

在桌面端进行交互式分析

对整个或部分软件项目运行静态代码分析。使用桌面工具生成报告，并对结果进行审核和分类。
使用类似调试器的视图步进运行时错误之前的每个语句，以找到复杂 Bug 的根本原因。组织和配置您的项目。Polyspace Code Prover 原生支持 60 多种 C 和 C++ 编译器，以及自动设置从项目的编译系统中提取的 Polyspace 分析。

文档