Polyspace Code Prover
证明软件中不存在运行时错误
Polyspace Code Prover 是一款可靠的静态分析工具，可以证明在 C 和 C++ 源代码中不存在溢出、被零除、数组访问越界和其他运行时错误。不需要执行程序、代码插装或测试用例即可产生结果。Polyspace Code Prover 使用基于形式化方法的语义分析和抽象解释，验证软件进程间、控制流和数据流行为。您可以用它来验证手写代码、生成的代码或两者的组合。每个代码语句都有颜色编码，表明是否无运行时错误、证明有缺陷、不可达或未经证明。
Polyspace Code Prover 显示变量和函数返回值的范围信息，并且可以证明哪些变量超出指定范围限制。代码验证结果可用来跟踪质量指标，并检查是否符合您的软件质量目标。Polyspace Code Prover 可与 Eclipse™ IDE 配合使用，在您的桌面上验证代码。
通过 IEC Certification Kit（符合 ISO 26262 和 IEC 61508）和 DO Qualification Kit（符合 DO-178），可提供对行业标准的支持。
使用形式化数学验证代码
实现无漏报的高质量水平和高安全级别
调用层次结构。
DO Qualification Kit。
理解和改进代码
减少在代码审查、调试和鲁棒性测试上花费的时间。
显示所有运行时条件下可能范围的提示框。
防止非预期软件行为
查找通过任何执行路径都无法访问的所有代码段以及逻辑和程序结构上的错误。
查找死代码。
将代码验证结果追溯到 Simulink 模型。
自动化代码验证流程
使用 Polyspace Code Prover Server™， 在带有构建自动化工具（如 Jenkins 和 Bamboo）的服务器级机器上运行 Polyspace Code Prover 静态分析引擎。
自动化代码验证流程。
通知并上传结果以供协同审查
将缺陷自动分配给组件所有者，发送电子邮件通知，并将结果上传到 Polyspace Code Prover Access，以便鉴别和解决问题。
发送附带 Polyspace Code Prover 结果的电子邮件通知。
查看 Polyspace Code Prover 结果以鉴别和解决问题
Polyspace Code Prover Access™ 提供 Web 浏览器界面，以便查看存储在中央存储库中的 Polyspace 代码验证结果和质量指标。 使用 Web 浏览器中的导航工具，检查随代码一起显示的代码验证结果。
检测运行时错误
项目质量和软件质量目标
控制板上显示的信息可用来监控软件质量、项目状态、缺陷数量、代码指标和软件质量目标。
项目概览控制板。
与您已经使用的缺陷跟踪工具集成
使用 Web 浏览器界面，在缺陷跟踪工具（如 Jira）中创建和分配工单。
创建工单。
最新特性
项目授权管理
创建和实施项目访问权的授权策略
AUTOSAR 支持
检查 AUTOSAR 规范与代码实现之间的运行时不匹配
堆栈大小计算
确定 C 程序和各个函数使用的最大堆栈
通过编译系统进行配置
通过编译系统自动生成 Polyspace 配置模块
多任务代码验证设置
将循环任务和非抢占式中断直接指定为验证选项
关于这些特性和相应函数的详细信息，请参阅发行说明。
