Why doesn't Polyspace(R2012b) report all overflows?

Simple code in my file running in multitasking verification mode with ep_task and interrupt_task as entry points.

The problem is that on variable c there is no overflow reported.

static signed char a;

static signed char b;

static signed char c;

/************************************ Periodic and interrupt functions ************************************/

void one_interrupt(void)
{
  a=127;
}

void t_10ms(void)
{
  a++;
  b++;
  c++;
}

void t_50ms(void)
{
  a=0;
}

/************************************** Entry point functions ********************************************/

void ep_task()

{

volatile int t;
  while(1)
  {
  t_10ms();

  t_10ms();

  t_10ms();

  t_10ms();

  t_10ms();

  t_50ms();
  }
}

void interrupt_task(void)
{
  while(1)
  {
    one_interrupt();
  }
}

/*********************************** Main function used as initialization  **********************************/

void main(void)
{ 
  a = 0;
  b = 0;
  c = 0;
}

Answer 1

[Alexandre De Barros]

Hi!

There is no overflow on c because there is another overflow on the variable b just before that stops the execution of t_10ms.

The first iterations in t_10ms for b and c are ok (and so these variables are incremented) but there is eventually an overflow on b. And because of this overflow, for Polyspace the execution of t_10m stops on the b++ statement. The overflow on c++ is then never reached, hence only the safe increments for c are given.

If you invert the b++ and c++ statements, you will see that this time b++ is green.

Alex

[Cristian Stancu]

Am I correct to assume that Polyspace will only show one overflow error per function ?

After that it will stop execution of that function therefore hiding all possible problems after the first confirmed issue?

In this case I am never sure that I have a complete report with Polyspace unless I solve all reported problems.