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,69c50fc0d29ced1b
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII
Path: 
 g2news2.google.com!postnews.google.com!v18g2000vbc.googlegroups.com!not-for-mail
From: Phil Thornley <phil.jpthornley@googlemail.com>
Newsgroups: comp.lang.ada
Subject: Re: Q: SPARK visibility rules and inherit annotations.
Date: Wed, 19 May 2010 08:54:56 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <568bb04d-6ad6-46da-9eb2-8d81c8c52b59@v18g2000vbc.googlegroups.com>
References: <4bf3fce5$0$2399$4d3efbfe@news.sover.net>
NNTP-Posting-Host: 80.177.171.182
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
X-Trace: posting.google.com 1274284497 15448 127.0.0.1 (19 May 2010 15:54:57
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Wed, 19 May 2010 15:54:57 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: v18g2000vbc.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 8.0; Windows NT 6.1; WOW64;
	Trident/4.0; SLCC2; .NET CLR 2.0.50727; .NET CLR 3.5.30729; .NET CLR
	3.0.30729; Media Center PC 6.0),gzip(gfe)
Xref: g2news2.google.com comp.lang.ada:11772
Date: 2010-05-19T08:54:56-07:00
List-Id: <comp.lang.ada>

On 19 May, 16:04, "Peter C. Chapin" <pcc482...@gmail.com> wrote:
> I'm working on a SPARK program. Right now I'm just doing design so my foc=
us is
> on package specifications; there are no package bodies. I'm having some
> trouble with the following:
>
> with TMLib.Cryptographic_Services;
>
> --# inherit TMLib.Cryptographic_Services;
> package TMLib.Credentials is
> =A0 =A0type Credential_Type is private;
>
> =A0 =A0-- Converts the raw bytes of a certificate transfer format to a cr=
edential.
> =A0 =A0procedure Certificate_To_Credential
> =A0 =A0 =A0(Raw_Data =A0 : in TMLib.Cryptographic_Services.Octet_Array;
> =A0 =A0 =A0 Credential : out Credential_Type;
> =A0 =A0 =A0 Valid =A0 =A0 =A0: out Boolean);
> =A0 =A0--# derives Credential from Raw_Data &
> =A0 =A0--# =A0 =A0 =A0 =A0 Valid =A0 =A0 =A0from Raw_Data;
>
> =A0 =A0-- Other stuff not shown here...
> end TMLib.Credentials;
>
> The SPARK Examiner complains about the use of "Cryptographic_Services" in=
 the
> declaration of the Raw_Data parameter to the procedure. Specifically I ge=
t
> error 754 that says (roughly) "The identifier Cryptographic_Services is n=
ot
> declared or not visible." I am then told that I probably need both a 'wit=
h'
> statement in the context clause and an 'inherit' annotation. Don't I have
> those things?
>
> Note that TMLib.Cryptographic_Services examines without error but it does
> generate a warning because the private section is empty and currently hid=
den
> from SPARK with a 'hide' annotation. It seems unlikely to me that has
> anything to do with my problem. Note that TMLib.Cryptographic_Services is=
 a
> public child of TMLib.
>
> I tried adding a 'with TMLib;' in the context clause but that didn't have=
 any
> effect. I realize the problem is probably something silly but I'm a bit
> baffled here. Any pointers would be appreciated.
>
> Thanks!
>
> Peter

Peter,

The problem comes from the reference in one child of TMLib to another
child of TMLib.

Where this is the case, in the code and annotations - but not in the
inherit or context clauses - the common parent must not appear in the
name.

So change the line:
   (Raw_Data   : in TMLib.Cryptographic_Services.Octet_Array;
to:
   (Raw_Data   : in Cryptographic_Services.Octet_Array;

This comes from the rule that no entity in a SPARK program can have
more than one name - and in the Ada this type can be called either
TMLib.Cryptographic_Services.Octet_Array or
Cryptographic_Services.Octet_Array.

In SPARK the decision was to enforce the second of these.

(I'm sure that this is one error message that could be improved...)

Cheers,

Phil