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,f5b7567796aaace6 X-Google-Attributes: gid103376,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!postnews.google.com!e25g2000prg.googlegroups.com!not-for-mail From: roderick.chapman@googlemail.com Newsgroups: comp.lang.ada Subject: Re: SPARK hide directive, hiding separate declaration. Date: Thu, 3 Jan 2008 19:16:11 -0800 (PST) Organization: http://groups.google.com Message-ID: References: NNTP-Posting-Host: 121.45.173.90 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit X-Trace: posting.google.com 1199416572 15735 127.0.0.1 (4 Jan 2008 03:16:12 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Fri, 4 Jan 2008 03:16:12 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: e25g2000prg.googlegroups.com; posting-host=121.45.173.90; 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.8.1.11) Gecko/20071127 Firefox/2.0.0.11,gzip(gfe),gzip(gfe) Xref: g2news1.google.com comp.lang.ada:19186 Date: 2008-01-03T19:16:11-08:00 List-Id: On Jan 3, 11:59 am, leeeruss...@gmail.com wrote: > Is there any thing like an --# unhide directive that would allow me to > let SPARK see the declaration in the body, but nothing else? Basically, the answer is "no". Once something is hidden, then that's that - it's Ada not SPARK. If you're hiding an entire package body, then the hide annotation is considered to hide the body AND any subunits of it. It's actually quite unusual to hide an entire package body, since if the entire body is Ada (not SPARK), then just don't submit it to the Examiner at all. If the package body is mostly SPARK with hidden subprograms, then move your subunit "up" into the SPARK part of the package body and analyse it there. All the best, Rod Chapman, SPARK Team, Praxis PS...if you're a supported SPARK customer, then such enquiries should _always_ be sent to sparkinfo@praxis-his.com - posting to comp.lang.ada does not guarantee a response (well..certainly not from SPARK Team anyway...)