在嵌入式开发中，代码静态分析工具相信大家应该都熟悉，都用过像PClint，understand C等，但对于动态验证，运行时错误验证工具还是不多，今天给大家介绍一款代码运行错误动态验证工具---Polyspace，本人有幸使用过这款优秀的软件，绝对不是广告噢呵呵，有兴趣的猿友可以到mathwork官网下载使用版，对你的代码进行验证，让你的代码更安全，更规范。Polyspace 目前已经被Mathwork 纳入麾下，称为mathwrok旗下的产品，如果各位以前用过matlab的话应该对mathwrok公司不陌生，Polyspace 分为Polyspace Code Prover 与 Polyspace Bug Finder两部分，可以结合使用。可以到mathwork官网搜索Polyspace下载试用版如下图所示：

Polyspace Code Prover™ 可以证明 C 和 C++ 源代码中不存在溢出、被零除、数组访问超出边界以及其他某些运行时错误。整个过程无需执行程序、植入代码，也不需要测试用例。Polyspace Code Prover 使用静态分析和基于形式化方法的抽象释义。该程序可以用于手写代码、生成的代码或二者的混合。每项操作均采用颜色标记，分别表示代码无运行时错误、已证明失效、无法达到或未经证明。

Polyspace Code Prover 还会显示变量和函数返回值的范围信息，并可以证明变量是否超出指定范围限制。这些结果可以发布到控制面板上，以跟踪质量指标并确保符合软件质量目标。Polyspace Code Prover 可以集成到构建系统中以执行自动验证。

• 主要特性

• 验证 C 和 C++ 嵌入式软件

• 检测运行时错误

• 查看范围信息

• 跟踪软件质量指标

• 依据代码验证结果回溯至 Simulink 模型

• 实现代码验证流程自动化

• 创建认证工件

检测运行时错误

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

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

跟踪软件质量指标

您可以定义一个集中式的质量模型，来跟踪运行时错误、代码复杂度和编码违规。使用这些指标，可以在代码从首次迭代到最终交付的完善过程中，持续跟踪预定义的软件质量目标。通过衡量代码质量改进率，Polyspace Code Prover 使开发人员、测试人员和项目经理能够致力于编写和交付高质量的代码。

实现代码验证流程自动化

通过将 Polyspace 整合到构建流程中，您可以将 Polyspace Code Prover 作为持续集成流程的一部分。您可以自动调度验证作业并设置电子邮件通知。您可以配置Polyspace Code Prover 将验证作业发布到集群计算机（使用 MATLAB Distributed Computing Server），并发送电子邮件通知结果。结果包含与上一版本代码的差异。这些差异由服务器自动计算。

您可以定义分析的频率、定义质量模型，指定需要分析的代码部分，以及接收结果的用户电子邮件地址。此外，您还可以定义自动验证需要涵盖构建过程的哪些特性。

Polyspace 可以生成各种格式的文档，如PDF， wrod，Html等等，方便归档汇报。还可以远程访问。最终生成的报告和结果 会显示代码的最终质量、高亮显示已审查的部分、生成代码指标、记录所使用的编码规则以及运行时错误状态。您可以将报告发布为 PDF、HTML、RTF 以及其他格式。