Polyspace Code Prover 快速入门

Polyspace^® Code Prover™ 可证明 C 和 C++ 源代码中不存在溢出、除以零、数组访问越界和某些其他运行时错误。它无需程序执行、代码插桩或测试用例即可生成结果。Polyspace Code Prover 使用基于形式化方法的静态分析和抽象解释。您可以将它应用于手写代码、生成的代码或这两者的组合。每个运算都进行了着色，以指示它是否存在运行时错误、是否已证明失败、是否不可达或是否未经证明。

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

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

教程

桌面端

• Run Polyspace Code Prover on Desktop
  Check C/C++ code exhaustively for run-time errors.
• Review Code Prover Results in Polyspace Platform User Interface
  Interpret Polyspace Code Prover results, fix code or justify results, manage results.

服务器端和 Web 界面

• Polyspace Server 和 Access 产品快速入门指南
  了解为工程、团队或组织设置 Polyspace 分析时要做的相关工作。
• 在服务器端运行 Polyspace Code Prover 并将结果上传到 Web 界面
  在提交后检查代码中是否存在运行时错误，并上传结果以便在 Web 界面中审查。

部署

• 使用 Polyspace Code Prover 进行源代码验证
  

  了解通过 Polyspace Code Prover 执行静态分析如何帮助您验证 C 和 C++ 代码。

• Polyspace 产品和软件开发工作流
  

  了解可以在软件开发生命周期中使用的 Polyspace 产品。

• Polyspace Bug Finder 与 Polyspace Code Prover 之间的差别
  

  了解 Bug Finder 与 Code Prover 如何互补，并确定何时在您的开发工作流中部署每种产品。