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) 实现对行业标准的支持。
教程
- 在桌面端运行 Polyspace Code Prover
详尽检查 C/C++ 代码是否存在运行时错误。 - 审查 Polyspace Code Prover 分析结果
解释 Polyspace Code Prover 结果，修复代码或对结果进行申述，管理结果。 - Polyspace 平台：用于静态分析和动态测试的统一平台
Polyspace 平台是一个使用 Polyspace 产品对 C/C++ 代码进行静态分析和测试的集成环境。 - Benefits and Limitations of Switching to Polyspace Platform User Interface
Import projects created in older user interface, run tests or static analysis on imported projects. - Run Polyspace Code Prover in Polyspace Platform User Interface
Check C/C++ code exhaustively for run-time errors. - Review Polyspace Code Prover Analysis Results in Polyspace Platform User Interface
Interpret Polyspace Code Prover results, fix code or justify results, manage results. - Polyspace Server 和 Access 产品快速入门指南
了解为工程、团队或组织设置 Polyspace 分析时要做的相关工作。 - 在服务器端运行 Polyspace Code Prover 并将结果上传到 Web 界面
在提交后检查代码中是否存在运行时错误，并上传结果以便在 Web 界面中审查。 - 在 Polyspace Access Web 界面中对结果进行分类和分配 (Polyspace Access)
在仪表板中导航，过滤结果，并将问题分配给团队成员。 - 发送包含 Polyspace Code Prover Server 结果的电子邮件通知
向开发人员发送电子邮件并在附件中包含指向 Polyspace 结果的链接。 - 在 Polyspace Access Web 界面中查看分配的结果 (Polyspace Access)
查看分配给您的检查结果。 - 将 Code Prover 分析从桌面端发送到本地托管的服务器端
将 Polyspace 分析负载转移到本地托管的服务器端并在桌面端审查下载的结果。
桌面端
Polyspace 平台用户界面
服务器端和 Web 界面
从桌面端到服务器端
部署
- 使用 Polyspace Code Prover 进行源代码验证
了解通过 Polyspace Code Prover 执行静态分析如何帮助您验证 C 和 C++ 代码。
- Polyspace 产品和软件开发工作流
了解可以在软件开发生命周期中使用的 Polyspace 产品。
- Polyspace Bug Finder 与 Polyspace Code Prover 之间的差别
了解 Bug Finder 与 Code Prover 如何互补，并确定何时在您的开发工作流中部署每种产品。
- 同时使用 Polyspace Bug Finder 和 Polyspace Code Prover 的工作流
在软件开发工作流中引入 Bug Finder 和 Code Prover 分析。
