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 Path: g2news2.google.com!postnews.google.com!p4g2000vba.googlegroups.com!not-for-mail From: Phil Thornley Newsgroups: comp.lang.ada Subject: Re: Representing errno in SPARK Date: Tue, 9 Jun 2009 09:03:42 -0700 (PDT) Organization: http://groups.google.com Message-ID: <51812f56-6c0a-407a-9f53-98c9b15f957c@p4g2000vba.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> 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 1244563423 4808 127.0.0.1 (9 Jun 2009 16:03:43 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Tue, 9 Jun 2009 16:03:43 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: p4g2000vba.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:6397 Date: 2009-06-09T09:03:42-07:00 List-Id: On Jun 9, 4:02=A0pm, xorquew...@googlemail.com wrote: ... > > Thank you, that's actually what I have here. The problem, however, > is that the package also has a body and SPARK doesn't seem to > like this: > > $ spark posix-error.ads posix-error.adb > ... > =A0304 =A0end POSIX.Error; > =A0 =A0 =A0 =A0 =A0 ^ > *** =A0 =A0 =A0 =A0Semantic Error =A0 =A0: 28: The own variable POSIX_err= no does > not have a > =A0 =A0 =A0 =A0 =A0 =A0definition [SR95 7.2.3]. > > Is it, by any chance, an issue due to Errno_Get and Errno_Set being > defined in the private section of the package spec? I think probably > not... No it's not that. 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. One possibility is to move the Errno abstraction and the two imported operations to another package internal to POSIX (but this means having an implementation for the POSIX versions of these subprograms). So: 1 - Remove the Import pragmas from POSIX spec. 2 - Create an internal package (eg POSIX.Internals) in the POSIX body that has the Errno abstraction and the imported subprograms. 3 - In the refinement annotation on the POSIX body put "--# own Errno is Internals.Errno;". 4 - Call through to these imported subprograms in the implementation of the subprograms that you now have to provide. (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 ...) Phil Thornley