Does Polyspace Prover's wrong analysis occur in a run-time loop execution ?

I have an orange warning in my source code reported by Polyspace Code Prover R2018a. But it is too weird and shown as below:

u4Data[] and ptMb->u4DFReg[] are using the same index (and this index is legal and equal to [0 .. 15]) to access the data arrays.

Could you (Technical support team) tell me what is the problem in the source code above ? And tell me how to resolve the warning ?

Thanks!

Answer 1

[John Boyd]

The ulDataReadSize variable is probably an unproven/unkown value and equal to full range. Since Polyspace is uncertain as to what the termination index is, it produced an orange on the first subscript that was out of bounds, in this case 16.