Polyspace Orange Check: Adding DRS for array

7 次查看(过去 30 天)
Hello guys,
I have this C++ code:
static char hw_type[4] = {'V','2',0, 0};
void myfunc()
{
hw_type[1]++;
}
This is how DRS is set, but it still show Overflow in Orange Check.
How to set the DRS value for array hw_type?
Thank you in advance

采纳的回答

Anirban
Anirban 2022-5-5
编辑:Anirban 2022-5-5
You have to select PERMANENT in the Init Mode column to get rid of the orange overflow.
  • When you select INIT, it means that hw_type starts with a range 2..3, but subsequent operations can take it outside that range.
  • When you select PERMANENT, it means that each time its value is unknown, Polyspace must assume that the unknown value continues to be in the range 2..3
Here is the full explanation. In your example, you do not have the complete application, that is, there is no main() function. So, Polyspace Code Prover has no information on the call contexts of myfunc(). For sound analysis, it has to assume that myfunc() can be called 0 or more times. As a result:
  • When you specify that hw_type starts with a range 2..3, the first time myfunc() is called, the ++ does not overflow, but after a certain number of calls, it does. If you see the tooltip on ++, you will see the range 2..127, indicating all possible starting values of hw_type in all calls to myfunc().
  • When you specify that hw_type has a permanent range of 2..3, each time myfunc() is called, it starts with that range of hw_type.
Hope that explains things.

更多回答(0 个)

类别

Help CenterFile Exchange 中查找有关 Troubleshooting in Polyspace Products for Ada 的更多信息

Community Treasure Hunt

Find the treasures in MATLAB Central and discover how the community can help you!

Start Hunting!

Translated by