How is a UNR check different from other types of checks that are colored Gray in PolySpace Client for C/C++ 6.0 (R2009a)?

When checking my code with PolySpace Client for C/C++ I see that there are UNR checks indicating unreachble operations in addition to regular checks in Gray color. What is the significance of UNR checks?

Answer 1

[MathWorks Support Team]

With UNR checks, PolySpace is able to detect very early in the process of its verification that the piece of code is unreachable and so instead of changing color of all checks in the unreachable branch; it puts only one check: a UNR check.

Now, a UNR could also happen on this kind of code: if (0) { x = 1; }.

Note that on this piece of code, without UNR, PolySpace does not put any check. This is also another reason why UNR has been introduced. In this case, it shows an unreachable branch.