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,FREEMAIL_FROM
	autolearn=ham autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,6d47e90d50b280da
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news2.google.com!postnews.google.com!q2g2000vbr.googlegroups.com!not-for-mail
From: Phil Thornley <phil.jpthornley@googlemail.com>
Newsgroups: comp.lang.ada
Subject: Re: Representing errno in SPARK
Date: Tue, 9 Jun 2009 10:26:53 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: <097700d6-31e1-421a-be30-56b026cd2da6@q2g2000vbr.googlegroups.com>
References: 
 <95bb6d31-f4fe-47c9-9274-72382ffad7ba@j32g2000yqh.googlegroups.com>
	<8a00d4ad-0ca3-4908-abf0-4fa980decb19@o36g2000vbi.googlegroups.com>
	<90f77911-389b-484e-b7f8-5f4d5e81e84e@y7g2000yqa.googlegroups.com>
	<51812f56-6c0a-407a-9f53-98c9b15f957c@p4g2000vba.googlegroups.com>
	<f5ea2a0d-3a2c-4ffa-89ba-f1619d671bb8@h28g2000yqd.googlegroups.com>
NNTP-Posting-Host: 80.177.171.182
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
X-Trace: posting.google.com 1244568414 19891 127.0.0.1 (9 Jun 2009 17:26:54
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Tue, 9 Jun 2009 17:26:54 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: q2g2000vbr.googlegroups.com; posting-host=80.177.171.182;
	posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 7.0; Windows NT 5.1;
	Trident/4.0; .NET CLR 1.1.4322; .NET CLR 2.0.50727),gzip(gfe),gzip(gfe)
Xref: g2news2.google.com comp.lang.ada:6399
Date: 2009-06-09T10:26:53-07:00
List-Id: <comp.lang.ada>

On 9 June, 17:11, xorquew...@googlemail.com wrote:
> Phil Thornley wrote:
> > What you are trying to do (by having other SPARK code in the body) is
> > mixing code that is inside and outside the 'SPARK boundary' in a
> > single package.
>
> I'm not entirely sure that's the case. The code in the body just maps
> errno values to enumeration values. I'd consider this code to be on
> the boundary at most (as opposed to any of it being "outside").
>
Well, the implementation of Errno is clearly outside the boundary and
any other code you are submitting to the Examiner must be inside the
boundary, by definition.
('On the boundary' would be a new concept for SPARK :-)
. . .

> > (A second possibility is simply to create an Errno in the package body
> > with a comment that it isn't actually used by the code ...)
>
> I did consider this but I wondered if this would cause issue with
> SPARK's
> flow analysis (as I'm only pretending to read/write a variable).

It shouldn't upset the flow analysis (but you will get compiler
warnings about unused data).

Phil Thornley