MATLAB: Do I receive an ORANGE ZDV check instead of a RED when the code segment being analyzed is certain to fail while using Polyspace Client for C/C++ 5.1 (R2008a+)

Polyspace Client for C/C++

When the following code is analysed using Polyspace Client for C/C++ 5.1 (R2008a):
void foo(int a)
{
int b;
b = 1/(a-8);
}
void foo3(int a)
{
int b;
b = 1/(a-3);
}
void bar(void)
{
int i;
for(i=0;i<10;i++)
{
foo(i);
}
}
#if 1
void baz(void)
{
int i;
for(i=0;i<10;i++)
{
foo3(i);
}
}
#endif
The checks generated are orange (instead of red) even though a divide by zero error (ZDV) is certain to occur in the above code.

Best Answer

The default precision of Polyspace Client for C/C++ 5.1 (R2008a) is not sufficient to generate RED checks (certain failures) in the particular case.
In order to workaround this issue, verify the results using the highest level of precision, i.e. using the -O3 flag.
Related Question