Re: [Spark] Converting Arrays

[Lutz Donnerhacke <lutz@iks-jena.de>]

* Rod Chapman wrote:
> A common trick in this case is to use a local,
> hidden procedure to initialise the out parameter:

Cool idea. I read the book yesterday evening till midnight and came to the
conclusion, that I have to replace Fullpath by a large constraint array.
This was obviosly wrong. You can always switch of Spark checkings when
running into trouble. :-/

But how can I write the required pre conditions?

          *******************************************************
                           Listing of SPARK Text
       SPARK95 Examiner with VC and RTC Generator Release 6.3 / 11.02
                           Demonstration Version
          *******************************************************


                       DATE : 11-MAR-2003 11:49:13.68

Line
   1  with Kernel.Linux_i86;
   2  --# inherit Kernel, Kernel.Linux_i86;
   3  
   4  package Kernel.IO is
   5     pragma Pure;
   6  
   7     subtype long is Linux_i86.long;
   8  
   9     type Fullpath is array(Positive range <>) of Character;
  10     procedure To_Fullpath (s : String; path : out Fullpath);
  11     --# derives path from s;
  12     --# pre s'Length < path'Length;
                            ^1
*** ( 1) Semantic Error:322: Only imports may be referenced in pre-conditions
         or return expressions.

  13     pragma Inline (To_Fullpath);
  14     pragma Inline_Always (To_Fullpath);
[...]
5 summarised warning(s), comprising:
     5 pragma(s)*
(*Note: the above warnings may affect the validity of the analysis.)