Re: [Spark] Arrays of Strings

[mheaney@on2.com (Matthew Heaney)]

rod.chapman@praxis-cs.co.uk (Rod Chapman) wrote in message news:<cf2c6063.0304110211.596b6b2b@posting.google.com>...
> Lutz Donnerhacke <lutz@iks-jena.de> wrote in message news:<slrnb95ehu.ob.lutz@taranis.iks-jena.de>...
> > In order to implement thin an execve binding, I wonder how to emulate the
> > C-Type "char const * const x []". Any bright ideas?
> 
> 
> Lutz and others,
>   Here are some thoughts and a possible solution to this problem.
> The execve() API is indeed a complex one for SPARK, since the
> type "pointer to unconstrained array of pointer to null terminated
> C String" is a tricky one for SPARK to model.

[Rod's example snipped]

Personally, I find Rod's solution way too heavy.

Why can't Spark model an access constant to a constant object?  For
example:

declare
   X : aliased constant String := "arg1";
   Y : aliased constant String := "arg2":

   type String_Constant_Access is 
     access constant String;

   type String_Constant_Access_Array is
     (Postiive range <>) of aliased String_Constant_Access;

   A : constant String_Constant_Access_Array := 
     (X'Access, Y'Access);
begin
   Op (A (A'First)'Access);
end;

Everything is static.  Yes, X and Y are aliased by the components of
array A, but neither X nor Y is variable, and the aliased view through
A is only a constant view.  So what's the problem?

I could understand your difficulty if X and Y were variable, but that
is not the case here.

I must say, I think the simplest solution is:

exec (filename, X);  -- for argv with one arg
exec (filename, X, Y); --for argv with two args
etc

and then turn off Spark checking in the body of exec.

Contrary to some of the views expressed in this thread, I find the C
syntax perfectly natural and perfectly elegant.  Rod's solution is
neither.