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