Specifications

Descriptions and examples of external specifications that can be checked with Code Prover

A Polyspace^® Code Prover™ analysis can check whether certain external specifications are violated. For instance, you can specify that certain variables in your code must not impact each other and let Code Prover determine if this specification is violated.

Polyspace Results

`Expected impact`	An object (source) is expected to have an impact on another object (sink)
`Expected absence of impact`	An object (source) is expected to have no impact on another object (sink)

Topics

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.