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

30 次查看（过去 30 天）
Shaku kaa
Shaku kaa 2016-9-19
评论： Mukesh Agarwal 2023-10-2
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?

请先登录，再回答此问题。

回答（2 个）

Christian Bard
Christian Bard 2016-11-2
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 2022-5-23
编辑：Anirban 2022-5-23
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 个评论
Mukesh Agarwal
Mukesh Agarwal 2023-10-2
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?

请先登录，再进行评论。

类别

在 Help Center 和 File Exchange 中查找有关 Options at Command Line Only 的更多信息

标签

产品

Community Treasure Hunt

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

Start Hunting!

Translated by