本帖最后由 hirain 于 2019-6-11 11:10 编辑

概述
        PolySpace 是 MathWorks 公司产品，主要用于分析软件运行时错误工具。它包括PolySpace Bug Finder 和PolySpace Code Prover 两个模块。

产品介绍
• PolySpace Bug Finder
        PolySpace Bug Finder 是静态代码分析软件，可以发现 C/C++ 代码中的各类缺陷，包括运行时错误，数据流问题，编程问题等各类代码缺陷。PolySpace Bug Finder 使用静态分析的方法分析软件控制，数据流和过程间的行为。可以在软件开发阶段就帮助开发人员发现并修正软件缺陷。
        PolySpace Bug Finder 可以生成软件代码静态度量报告，包括发现的缺陷，编码规范不合规项和代码质量信息比如圈复杂度。为了方便使用，PolySpace Bug Finder 还提供了和 Eclipse IDE 开发环境及用户的构建系统集成的功能。
        通过 IEC Certifcation Kit（IEC 61508和 ISO 26262），PolySpace 提供对相关工业标准认证的支持。同时，PolySpace 支持 Ada 语言的代码检查。


• PolySpace Code Prover
        PolySpace Code Prover 证明 C/C++ 代码中不含有溢出，除零，数组越界等特定的运行时错误。它不需要运行代码，代码插装和测试用例。PolySpace Code Prover 使用静态分析和形式化的抽象解释方法，适用于手写代码，自动生成代码和两者都有的混合代码。结果采用颜色表示代码中是否没有运行时错误，被证明的错误，不可达代码和未经证明的代码。
        PolySpace Code Prover 使用抽象解释和静态分析方法来证明，识别和分析运行时错误，例如溢出，除零和指针的越界。这个技术综合完整的验证所有的运行条件并自动的证明代码是被证明的（安全的，错误的，不可达的）和未经证明的。PolySpace Code Prover 的检查结果用颜色来标识。
        能够发现的错误包括：
    ♦ 溢出，除零及其它的数学错误
    ♦ 数组访问越界和非法的指针取消引用
    ♦ 总是 True/False 的语句
    ♦ 类成员无初始化 (C++)
    ♦ 读取未初始化的数据
    ♦ 访问 null this 指针 (C++)
    ♦ 死代码
    ♦ 与面向对象编程，继承和错误处理有关的动态错误 (C++)