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

59 views (last 30 days)
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?

Answers (2)

Christian Bard
Christian Bard on 2 Nov 2016
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

Anirban
Anirban on 23 May 2022
Edited: Anirban on 23 May 2022
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.
  1 Comment
Mukesh Agarwal
Mukesh Agarwal on 2 Oct 2023
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?

Sign in to comment.

Community Treasure Hunt

Find the treasures in MATLAB Central and discover how the community can help you!

Start Hunting!