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: 103376,7b0188e023be40b6 X-Google-Attributes: gid103376,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII Path: g2news2.google.com!postnews.google.com!y13g2000yqn.googlegroups.com!not-for-mail From: roderick.chapman@googlemail.com Newsgroups: comp.lang.ada Subject: Re: SPARK Examiner -- visibility of Ada.Strings.Unbounded (and probably lots of other packages) Date: Thu, 26 Mar 2009 08:35:15 -0700 (PDT) Organization: http://groups.google.com Message-ID: References: <8c753bd7-3df6-418a-8cd7-342af6eadeff@g38g2000yqd.googlegroups.com> <49cb9cd8$0$31344$9b4e6d93@newsspool4.arcor-online.net> NNTP-Posting-Host: 217.205.167.137 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: posting.google.com 1238081715 387 127.0.0.1 (26 Mar 2009 15:35:15 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Thu, 26 Mar 2009 15:35:15 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: y13g2000yqn.googlegroups.com; posting-host=217.205.167.137; posting-account=HCzrEgkAAABSfGsTnv-u5wET6EzuneVi User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-GB; rv:1.9.0.7) Gecko/2009021910 Firefox/3.0.7,gzip(gfe),gzip(gfe) Xref: g2news2.google.com comp.lang.ada:5310 Date: 2009-03-26T08:35:15-07:00 List-Id: On Mar 26, 3:18=A0pm, Georg Bauhaus wrote: > My outdated copy of the SPARK book describe a Spark I/O package. > Also, package Interfaces does not pass, so if that is an important > base for run-time support ... You'll need what we call a "shadow" package specification that offers a SPARK-friendly (i.e. legal SPARK) version of an otherwise non-SPARK package. You then use the Examiner's "index file" mechamisn to make the Examiner read in the shadow specification, while your compiler, of course, uses the "real" Ada version. More info in the book in section 13.1. Ada.Strings.Unbounded is likely to be very hard to shadow, though, since it is full on non-SPARK things like String_Access and returning String from a function, which is beyond the run-time library profile support by SPARK. Same goes for Interfaces - most of it is legal SPARK, but (in GNAT anyway) the overloading of the various Shift_ and Rotate_ functions is not legal in SPARK. If you really need access to those things, then create a "thick binding" that "un-overloads" those functions in a distinct package. SPARK_IO is an example of this - it offers a thick-binding to the underlying Ada.Text_IO package. - Rod Chapman, SPARK Team