PolySpace bug finder approximations

Hello! could you help me?

In polyspace help i found information:

-------------------------------------------

Considering the Effects of Application Code Size. Polyspace can make approximations Polyspace can make approximations when computing the possible values of the variables, at any point in the program. Such an approximation use a superset of the actual possible values.

For instance, in a relatively small application, Polyspace software can retain detailed information about the data at a particular point in the code. For example, the variable VAR can take the values

{ –2 ; 1 ; 2 ; 10 ; 15 ; 16 ; 17 ; 25 }

If the code uses VAR to divide, the division is green (because 0 is not a possible value).

If the program is large, Polyspace software simplifies the internal data representation by using a less precise approximation, such as:

[-2 ; 2] U {10} U [15 ; 17] U {25}

----------------------------------------------

And thats what i see in my project for several important variables.

I can not change this PolySpace settings (Precision level 3, Verification level 2, Respect types in fields on and Respect types in global variables on) without big reason and evidence. I can not change my code.

Can i change this part of behavior of PolySpace somehow? Can i reduce "using a less precise approximation"

Runtime and memory not a big problem.

Answer 1

[Shubham]

Hi Andrei

I understand you want to increase the precision of the approximation of the values of the variables without changing the specified Polyspace Configuration settings.

The precison of approximation depends on several factors and size of the application is one of them. The way to increase the approximation in this case is to increase the Precision Level 3 and verification level 4. It will increase the complexity so will take more time.

But since you are not supposed to change the configuration settings, there is no assured way to acheive this. You can try reducing the size of the application but again the effect is not guaranteed.

Hope this helps.