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=unavailable autolearn_force=no version=3.4.4
X-Received: by 2002:a37:7a84:: with SMTP id
 v126mr7494717qkc.423.1585223763761;
        Thu, 26 Mar 2020 04:56:03 -0700 (PDT)
X-Received: by 2002:a9d:709a:: with SMTP id l26mr5668878otj.240.1585223763514;
 Thu, 26 Mar 2020 04:56:03 -0700 (PDT)
Path: 
 eternal-september.org!reader01.eternal-september.org!feeder.eternal-september.org!news.gegeweb.eu!gegeweb.org!usenet-fr.net!proxad.net!feeder1-2.proxad.net!209.85.160.216.MISMATCH!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Thu, 26 Mar 2020 04:56:03 -0700 (PDT)
In-Reply-To: <lyr1xfl9h2.fsf@pushface.org>
Complaints-To: groups-abuse@google.com
Injection-Info: google-groups.googlegroups.com; posting-host=80.189.116.65;
 posting-account=7NSrMAoAAACQXGDiUf5Zzn18ZM31fxb5
NNTP-Posting-Host: 80.189.116.65
References: <aa72dccb-e291-4849-ad37-9d001fad7234@googlegroups.com>
 <2cf70068-45e1-4e39-8ff4-3348f37e63fd@googlegroups.com>
 <f9bf574c-af41-4d66-8c22-d4e83ed8ab7a@googlegroups.com>
 <lyr1xfl9h2.fsf@pushface.org>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <a552d00c-39f2-4dc7-85b8-4b663405e363@googlegroups.com>
Subject: Re: How do I resolve SPARK warning "procedure [...] has no effect for
 output procedure
From: digitig <digitig@gmail.com>
Injection-Date: Thu, 26 Mar 2020 11:56:03 +0000
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
Xref: reader01.eternal-september.org comp.lang.ada:58250
Date: 2020-03-26T04:56:03-07:00
List-Id: <comp.lang.ada>

On Thursday, March 26, 2020 at 10:02:52 AM UTC, Simon Wright wrote:
> digitig <digitig@gmail.com> writes:
>=20
> > When I run SPARK examiner (from within GPS) I Get the warning I'd like
> > to clear:
> >
> > warning: subprogram "Error_Header" has no effect.
>=20
> Try
>=20
>    package Utils with Spark_Mode is
>       pragma Warnings (Off, "has no effect");
>       procedure Error_Header;
>       pragma Warnings (On, "has no effect");
>    end Utils;

I specifically said I wanted to resolve it, not hide it ("Hopefully better =
than `SPARK_mode =3D> Off'").

I've found out how in older versions of SPARK I could annotate the procedur=
e to say that it modified global outputs, but that depended on SPARK_Io, an=
d the documentation on that says it has been replaced and I can't find eith=
er it or its replacement - the current SPARK documentation doesn't seem to =
mention either.