How does Polyspace handle the RED and GREEN checks on detecting loop constructs in a source code, in Polyspace Client for C/C++ 8.2 (R2011b) ?

Everytime Polyspace detects red and green cases for a loop, Polyspace wouldn't mark this loop as infinite (red error). I understand that, its the way Polyspace handles loops in general.

int main(void)

{

     volatile LKuint16 rnd = 0;

     volatile LKuint16 par = 0;

     int res;

     if (rnd) res = UDS_u8GetDataIdLength(par); // call only with 0

     return res;

}

I have also run a new analysis with the option:

-prepare-automatic-tests

and I was able to start the Automatic Orange Tester. There's no orange warning either concerning the loop or concerning the input parameter of the function.

Answer 1

[MathWorks Support Team]

In a scenario when a function call is dictated by a conditional check, its possible that a parameter to the IF condition could be 0, but can also have many other values. So you have two workflows here and Polyspace cannot put a red in function:

1. with value 0, we have a for ever loop: red

2. with value greater or equal to the parameter to the function we have no for ever loop: green

So for a loop construct, red+green means no red and tooltip shows that Polyspace does not know number of maximum possible iterations on loop.

May be using the option -prepare-automatic-tests and launching the Automatic Orange Tester GUI on results, would highlight this for ever loop but there is no guarantee as tests are completely random and should call function with value 0.