规范

可以使用 Code Prover 检查的外部规范的描述和示例

Polyspace^® Code Prover™ 分析可以检查是否违反了某些外部规范。例如，您可以指定您的代码中的某些变量不得相互影响，并让 Code Prover 确定是否违反了此规范。

Polyspace 结果

`预期有影响`	An object (source) is expected to have an impact on another object (sink)
`预期无影响`	An object (source) is expected to have no impact on another object (sink)

Prove Absence of Impact Between Objects in C/C++ Program
Set up impact analysis in Polyspace Code Prover, define sources and sinks.
Review Results of Impact Analysis in Polyspace Code Prover
Trace path from source of impact to sink, find all sinks impacted by a source and vice versa.