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,start
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news2.google.com!postnews.google.com!h28g2000yqd.googlegroups.com!not-for-mail
From: xorquewasp@googlemail.com
Newsgroups: comp.lang.ada
Subject: Minor SPARK problem concerning 'redundant' with clauses.
Date: Wed, 10 Jun 2009 12:31:48 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <d159ba39-a898-42fb-bb2b-a3b5142893d3@h28g2000yqd.googlegroups.com>
NNTP-Posting-Host: 81.86.41.187
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
X-Trace: posting.google.com 1244662309 16512 127.0.0.1 (10 Jun 2009 19:31:49
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Wed, 10 Jun 2009 19:31:49 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: h28g2000yqd.googlegroups.com; posting-host=81.86.41.187;
	posting-account=D9GNUgoAAAAmg7CCIh9FhKHNAJmHypsp
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.0.7)
	Gecko/2009030814 Iceweasel/3.0.9 (Debian-3.0.9-1),gzip(gfe),gzip(gfe)
Xref: g2news2.google.com comp.lang.ada:6418
Date: 2009-06-10T12:31:48-07:00
List-Id: <comp.lang.ada>

I have a package P1 that uses the value of a constant defined in P2.

SPARK requires me to --# inherit P2 and the only place the annotation
can appear is in the spec of P1. The Ada compiler, however, sees that
the constant is only referenced in the body and complains loudly that
the 'with' clause is redundant and might be moved into the body of P2.

Is there a sensible solution to stop the two systems treading on each
other like this? In most cases, I can hack around the problem with a
spurious 'use type' clause (as much as I dislike it).

I tried to use pragma Warnings (Off) to wrap the "redundant" with
clauses, but of course SPARK immediately rejected it:

***        Syntax Error      : No complete PRAGMA_REP can be followed
by
           reserved word "WITH" here.