How is this DRS (Data Range Specification )in Polyspace code prover is generated?

hi, i want to know how this DRS in Polyspace Code Prover is generated. In my code , i have Global Variable of array size 8 but, in the DRS window it is showing only one element of that array to add min & max value(it is not showing its size within the "[ ]"). is it possible to view all the other elements of that array ? is it possible to get DRS option for all the other elements? if so, how to do it?

Answer 1

[Christian Bard]

Hi Shaku,

Actually that is not possible to give a min/max range for each element of an array using data range specifications. You may write a function that initialize elements of array, and Polyspace Code Prover, will certainly take it into account.

Regards, Christian

Answer 2

[Anirban]

Even though the array size does not appear in the Data Range Specifications window, you can specify the same constraint on all array elements using that window. What you cannot do is specify different constraints on individual array elements (typically, there is no reason to do that anyway since all array elements are supposed to be similar).

Here is an example:

int arr[8];

int getFourthElement() {
  return arr[4];
}

If you specify a permanent constraint of [-1..1] on the array arr as shown below, in your results, you will see that the return value of getFourthElement is in that range.

[Mukesh Agarwal]

Hi Anirban,

I have 1 use case where all array should not have same specification. If array is for breakpoint of LUT then it must be monotonically increasing. When Breapoint array is given same specification then this cannot be guaranteed.

Do you have any other solution to deal with this other then Stubbibg LUTs?