用于Ada的Polyspace客户端™证明了Ada83和Ada95源代码中没有溢出、被零除、越界数组访问和某些其他运行时错误。它产生的结果不需要程序执行、代码插装或测试用例。Ada的Polyspace客户端使用基于形式化方法的抽象解释技术来验证代码。分析结果显示在源代码中。每个代码语句都用颜色编码，以指示它是否没有运行时错误、已证明失败、不可访问或未证明。用于Ada的Polyspace客户端显示变量和函数返回值的范围信息，并可以证明哪些变量超出了指定的范围限制。
您可以在您的桌面上使用Ada的Polyspace Client在编译和测试之前运行和检查代码分析。
证明没有关键的运行时错误
检查Ada83或Ada95代码操作的运行时正确性。确定永远不会出现运行时错误的语句，而不管运行时条件如何。在事件跟踪、变量值范围和与发现相关的调用树的支持下分析运行时漏洞。Ada的Polyspace客户端使用形式化的方法来检测无法通过其他方法进行测试的错误。在不执行代码的情况下，根据所有可能的输入分析所有代码路径。
桌面交互分析
组织和配置您的项目，并在软件项目的子集上运行静态代码分析，在将代码提交到源代码存储库之前确认代码更改。使用Polyspace客户端为Ada生成报告，并审查和分诊结果。使用类似调试器的视图查找复杂bug的根本原因，逐步浏览导致运行时错误的每个语句。
静态应用程序安全测试
通过充分强调潜在的脆弱Ada语句(如内存访问、缓冲区溢出或数值溢出)，证明应用程序不存在关键的安全漏洞。支持20条CWE弱点规则。利用Ada的Polyspace Client的分析结果来补充或取代模糊测试，并将重点放在易受攻击的识别操作上。
改进和补充鲁棒性和功能测试
使用Ada的Polyspace Client来改进鲁棒性测试，方法是将测试集中在被证明不安全的语句上，例如除以零或溢出。使用Ada的Polyspace客户机的结果来创建和维护边界和分区测试，利用控制和数据流分析，以及函数参数和全局变量的计算范围。
产品资源:
您也可以从以下列表中选择网站: