Polyspace (either bug finder or code prover) is capable of detecting overflow on iteration variable?

I have a compiler reported bug stating that a loop may iterate more than expected. It is quite a corner case, but when dealing with ISO26262, corner cases need to be taken into consideration. Now I wonder if Polyspace could help to anticipate the issue. Would it detect and report about an overflow in the following code construct:

for (uint8_t i=100;i>1;i+=255) do_something();

Answer 1

[Anirban]

Hi Victor,

Both Bug Finder and Code Prover can detect this issue.

• If you run Bug Finder, you will see a result Unsigned integer conversion overflow coming from conversion of (i + 255) to uint8_t.
• If you run Code Prover with the option -unsigned-integer-overflows forbid (or warn-with-wrap-around), you will see a red (or orange) Overflow. For details on the option, see -unsigned-integer-overflows. Since the Standard specifies wrap-around behavior for unsigned integers, the default Code Prover behavior is to allow overflows for unsigned integers (with a wrapped value). But using the option, you can change this default behavior.

Code Prover is more exhaustive than Bug Finder, so it will try to detect all possible overflows in all contexts (subject to documented assumptions), not just in this simple situation. Depending on the level of exhaustiveness you want and the critical nature of your application, you can choose either product. See more on the differences between Bug Finder and Code Prover in the documentation.