in polyspace why pointers assignation fails

if I have this code : u8MyArray[10]; u8 * pu8FirstPointer; u8 * pu8Data; u8 u8Index; pu8FirstPointer = u8MyArray; while( u8Index <10) { *pu8FirstPointer = *pu8Data; pu8FirstPointer ++ ; pu8Data++; }

this code is supposed to copy the data to the array but polyspace doesn't get it ,why?

Answer 1

[Christian Bard]

With the following code, and with default options, Polyspace Code Prover (release R2013b) "got" it:

typedef unsigned char u8;
u8 u8Dest[10]; 
u8 u8Source[10];

void foo(void)
{ 
  u8 * pu8FirstPointer; 
  u8 * pu8Data; 
  u8 u8Index = 0; 
  pu8FirstPointer = u8Dest;
  pu8Data = u8Source;
  
  while( u8Index <10) { 
    *pu8FirstPointer = *pu8Data; 
    pu8FirstPointer ++ ; 
    pu8Data++; 
    u8Index++;
  }
}

So, would you please, contact www.mathworks.com/support with options used, realease and some explanation about what do you mean by "Polyspace doesn't get it".