可以设置以下选项来帮助你:
1。(17日)之前“优化大型静态初始化器”(内部选项名称:-no-fold)
当定义变量与巨大的静态初始化、规模问题可能发生在编译阶段。这个选项接近初始化数组类型的整数、浮点数和char类型(包括字符串)。它可以加快分析,但对于某些应用程序可能会降低精度
没有设置默认值:选项。
Shell脚本条目示例:
(R2013b之前)polyspace-c -no-fold……
(因为R2013b) polyspace-code-prover-nodesktop -no-fold……
2。“精度水平”(o)
这个选项指定要使用的精度水平。它提供了更高的选择性,以换取更多的分析时间,因此使评估结果更有效率,因此使bug的代码更容易分离。它是通过指定算法用于模型在分析程序状态空间。
建议分析应该开始低精度。红色和灰色的代码错误可以解决重启Polyspace使用这个选项之前,应用精密水平仪如下所述。
好处——更高的精度水平有助于更高的选择性,使评估结果更有效率,因此使bug的代码更容易分离。——更高的精度水平也意味着更高的分析时间
o0对应于静力区间分析。
o1群对应于复杂的多面体模型的域值。
- 02密切对应于更复杂的算法模型域值(一个混合的方法与整数格和复杂的多面体)。
o3只适合小型的代码。这样的代码,生成的选择性可能达到高值,如98%,导致很长时间分析,如一个小时每1000行代码。
默认值:- 02
3所示。(17日)之前“减少任务复杂性”(-lightweight-thread-model)多任务验证。
可以简化任务建模Polyspace内部代码验证。
其他选项可用“额外选项”(指定在“其他Polyspace选项)因为R2013b或常规的早期版本的选项:
4所示。验证内部结构的“深度”(-k-limiting)
这是一个扩展选项限制分析的深度嵌套结构在指针分析。
此选项只用于Polyspace C和c++。
默认值:没有固定的限制。
Shell脚本条目示例:
polyspace-code-prover-nodesktop -k-limiting 1…
在上面这个例子中,将精确分析只有一个嵌套的水平。
3所示。-respect-types-in-fields
这是一个扩展选项,旨在帮助处理复杂的代码。应用时,Polyspace假设结构字段不包含指针从未用于控股声明为指针值。这个选项应该只使用类型安全的C / c++代码,不造成损失的精度。参见-respect-types-in-globals
默认值:Polyspace假定结构字段可能包含指针值。
4所示。-respect-type-in-globals
这是一个扩展选项,旨在帮助处理复杂的代码。应用时,Polyspace假设全局变量不包含指针从未用于控股声明为指针值。这个选项应该只使用类型安全的C / c++代码,不造成损失的精度。也看到-respect-types-in-fields。
默认值:Polyspace假定全局变量可以包含指针的值。
请注意,当面对内存不足问题,recommandation是减少应用程序的大小Polyspace。
这是本文中解释:
