Polyspace Code Prover

检测运行时错误

Polyspace Code Prover 将抽象释义与静态代码分析结合使用,以识别和诊断溢出、被零除和指针越界等运行时错误。这项技术可以完整而全面验证所有运行时情况,并为每项代码自动提供诊断报告,包括已证明、已失败、无法达到或未经证明诊断。在 Polyspace Code Prover 生成的验证结果中,每一项 C 或 C++ 运算均采用颜色编码表示其状态:

绿色: 已证明没有运行时错误
红色:已证明在每次运行时都有错误
灰色:已证明无法达到(可能表示存在功能性问题)
橙色:未经证明,在某些情况下可能有错

Color-coded run-time error attributes identified by Polyspace Code Prover.

Polyspace Code Prover 识别的运行时错误属性。

检测到的错误包括:

  • 溢出、下溢、被零除和其他运算错误
  • 数组访问超出边界和非法引用指针
  • Always true/Always false 语句
  • 未初始化的类成员 (C++)
  • 读取对未初始化数据
  • 访问空 this 指针 (C++)
  • 死代码
  • 与对象编程、继承和异常处理有关的动态错误 (C++)
下一页: 查看范围信息

试用 Polyspace Code Prover

获取试用版软件

Comprehensive Static Analysis Using Polyspace Products

观看网上技术交流会录像