规模

指定验证规模

要对特定代码构造进行更深入或更粗浅的分析，请使用规模选项。有时，使用这些选项会显著改变验证时间。

Polyspace 选项

`内联 (-inline)`	指定必须要为对其的每次调用在内部创建克隆的函数
`结构体内部的验证深度 (-k-limiting)`	限制对嵌套结构体的分析深度