Re: Question about out parameters of unconstrained array type.

[Alexander Senier <mail@senier.net>]

On Sun, 26 Feb 2012 09:14:53 -0000
Phil Thornley <phil.jpthornley@gmail.com> wrote:

> For your code above, if the cost of including the initialization of the 
> array is too high then the easiest way to remove the the error is 
> probably to add another parameter that is the length of the Description 
> string. Using Alexander's code:

Can anybody comment on the legality of using attributes of an out parameter of
an unconstrained (array) type in Ada? A brief skim through LRM could not
enlighten me...

If using 'Length (and other attributes) elsewhere than in a loop constraint
actually is legal Ada, than this seems like an unnecessary limitation of SPARK
that should be relaxed. For now, I would prefer accepting the resulting flow
error for several reasons:

* Default initialization may hide subsequent flow errors that would
  been spotted by the flow analysis otherwise (the coarse grained treatment
  of array makes that less important, though)

* As Phil said, (additional) default initialization may impose a significant
  performance overhead

* Passing in the upper bound of the array as a parameter IMHO makes the code
  less intuitive and readable than it could be - just to silence the flow
  analysis ;-(

Regards
Alex