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,cbe0aa3013785791 X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news2.google.com!postnews.google.com!21g2000vbk.googlegroups.com!not-for-mail From: Robin Messer Newsgroups: comp.lang.ada Subject: Re: Minor SPARK problem concerning 'redundant' with clauses. Date: Thu, 11 Jun 2009 01:52:20 -0700 (PDT) Organization: http://groups.google.com Message-ID: <0dbb205a-71fd-4b06-a99e-e6c2c9b27fa8@21g2000vbk.googlegroups.com> References: <445038cd-3a8b-4222-a49b-3b64d4fc3c72@r3g2000vbp.googlegroups.com> NNTP-Posting-Host: 217.205.167.137 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit X-Trace: posting.google.com 1244710341 1346 127.0.0.1 (11 Jun 2009 08:52:21 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Thu, 11 Jun 2009 08:52:21 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: 21g2000vbk.googlegroups.com; posting-host=217.205.167.137; posting-account=eI6N8QoAAAAnb-Cxkz1eKRT9XZ_FT5ri User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-GB; rv:1.9.0.10) Gecko/2009042316 Firefox/3.0.10,gzip(gfe),gzip(gfe) Xref: g2news2.google.com comp.lang.ada:6430 Date: 2009-06-11T01:52:20-07:00 List-Id: Britt is right. The correct solution is to move the "with" to the package body. As an aside, the SPARK Examiner recognises certain pragmas, but in the majority of cases it just issues a warning and continues its analysis. It is, however, a bit more fussy about where pragmas can be placed. The following code is accepted by the Examiner (with a warning about the pragma). pragma Warnings (Off); with Q; --# inherit Q; package P is type T is range 0 .. 100; end P; -- Robin