Re: How do functions return unbounded arrays?

[Rod Chapman <rod@praxis-cs.co.uk>]

> They are in general forbidden in SPARK.
> However, the "&" operator is allowed on string literals as you would expect a
> compiler to handle this case statically.

Your mileage varies...

In Ada83, things which you "expect the compiler to handle statically" often
aren't.  Some compilers are better at spotting static expressions
above-and-beyond
what is strictly required by the Ada83 LRM (e.g. XD-Ada).  Some stick more
closely
to the letter of the law and generate more dynamic code for expressions even if
they
_could_ be evaluated statically (e.g. the "old" Alsys technology)

In Ada95 (and thus SPARK95), things are much better, since the definition
of "static" covers a much larger set of expressions, and the RM's implementation
advice gives you a pretty clear idea of what to expect.

For critical and real-time work, I _always_ check with the compiler vendor
and/or read the generated code for these bits of the language.
 -  Rod Chapman
   rod@praxis-cs.co.uk