From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,463c5796782db6d8
X-Google-Attributes: gid103376,public
X-Google-ArrivalTime: 2003-04-11 11:41:34 PST
Path: archiver1.google.com!postnews1.google.com!not-for-mail
From: mheaney@on2.com (Matthew Heaney)
Newsgroups: comp.lang.ada
Subject: Re: [Spark] Arrays of Strings
Date: 11 Apr 2003 11:41:34 -0700
Organization: http://groups.google.com/
Message-ID: <1ec946d1.0304111041.7edae9a@posting.google.com>
References: <slrnb95ehu.ob.lutz@taranis.iks-jena.de>
 <cf2c6063.0304110211.596b6b2b@posting.google.com>
NNTP-Posting-Host: 66.162.65.162
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 8bit
X-Trace: posting.google.com 1050086494 29122 127.0.0.1 (11 Apr 2003 18:41:34
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: 11 Apr 2003 18:41:34 GMT
Xref: archiver1.google.com comp.lang.ada:36095
Date: 2003-04-11T18:41:34+00:00
List-Id: <comp.lang.ada>

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.