precision loss in read of 2d array in Polyspace R2021b code prover

Hello,

I defined the range in DRS for my 2d array (f.e. const int16 array[2][5], and in DRS array 0 32000 permanent), and the array will be used as Pointer used Tabfct(..., &array[0][0],...). and Tabfct is simply defined as:

int16 Tabfct (..., const int16 * z_table, ...)

{

return z_table[0];

}

and I put the function Tabfct as inline function. And I got warning in log: precision loss in read of (*Tabfct:z_table)+0 because (*Tabfct:z_table)+0 may point to volatile data. and Polyspace says that the range of Tabfct is fullrange [-32768..32767].

If array is 1d, like array[5], I got the right range for the function Tabfct and no warning.

I used polyspace 2017b, it was no Problem for 2d array. But in 2021b I can not get the right range. Could you please tell me why or what should I do.

My purpose: the function Tabfct to stub, so the Polyspace knows that, Tabfct has the same range like array.

Answer 1

[Sachin Lodhi]

Based on my understanding, it appears that you obtained the correct ranges in Polyspace R2017b, but not in R2021b. I want to inform you that this is a known issue, and our team is actively working on resolving it in future releases. We have created an enhancement request to address this behaviour specifically in Polyspace R2021b going forward.

To ensure a smoother experience and benefit from bug fixes and significant performance optimizations, I would recommend considering an upgrade to Polyspace R2022b or a later version. This will provide you with the latest improvements and enhancements.