Polyspace Orange Check: Adding DRS for array

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

Answer 1

[Anirban]

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.

[Zulham Mr]

It works.

Thank you.