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

조회 수: 57(최근 30일)
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.

Community Treasure Hunt

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

Start Hunting!

Translated by