Polyspace 使关键代码安全可靠

Polyspace

®

  静态代码分析产品使用形式化方法来证明一切可能的控制流和数据流在缺乏关键的运行时错误。它们包括用于编码规则的检查程序，安全漏洞，代码指标以及数百种其他类型的错误。

https://ww2.mathworks.cn/products/polyspace.html

今天新发现的一个组件。今天我重装了MATLAB2018A发现的

大家可以探索一下。

证明软件中不存在运行时错误

Polyspace Code Prover™ 作为一款可靠的静态分析工具，能够证明在C 和 C++ 源代码中不存在溢出、除零、数组访问越界以及其它运行时错误。整个分析过程无需执行程序、植入代码，或运行测试用例。Polyspace Code Prover 使用基于形式化方法的语义分析和抽象解释验证软件程序交互、控制和数据流的行为。你可以用于手写代码、生成代码或二者的混合代码。每项检查均在代码上着色表示是否无运行时错误、已证明有问题、不可达或有待进一步分析。

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

通过IEC Certification Kit（适用于 IEC 61508 和 ISO 26262）和 DO Qualification Kit（适用于 DO-178）可以提供对行业标准的支持。此外，它还可以支持 Ada 语言。

功能还是很强大的。

再说一次最新版的好处：你不用记绘图函数了

选择你要表现的数据点对应的图就行了。然后可以设置不同数据对应的坐标轴。

请教下这种静态代码解析问题要怎么解决呢？ 就是bootloader跳转到app，调用了一个绝对地址跳转，要怎么写才不会违反规则？  谢谢！