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

Question

Victor Garcia Santos 2020-6-9

0
链接

此问题的直接链接

https://ww2.mathworks.cn/matlabcentral/answers/545009-polyspace-either-bug-finder-or-code-prover-is-capable-of-detecting-overflow-on-iteration-variable

编辑： Anirban 2020-6-9

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();

0 个评论
显示 -2更早的评论隐藏 -2更早的评论

请先登录，再进行评论。

请先登录，再回答此问题。

Answer 1

Anirban 2020-6-9

0
链接

此回答的直接链接

https://ww2.mathworks.cn/matlabcentral/answers/545009-polyspace-either-bug-finder-or-code-prover-is-capable-of-detecting-overflow-on-iteration-variable#answer_448757

编辑：Anirban 2020-6-9

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.