From: digitig <digitig@gmail.com>
Subject: Re: How do I resolve SPARK warning "procedure [...] has no effect for output procedure
Date: Thu, 26 Mar 2020 04:56:03 -0700 (PDT)
Date: 2020-03-26T04:56:03-07:00 [thread overview]
Message-ID: <a552d00c-39f2-4dc7-85b8-4b663405e363@googlegroups.com> (raw)
In-Reply-To: <lyr1xfl9h2.fsf@pushface.org>
On Thursday, March 26, 2020 at 10:02:52 AM UTC, Simon Wright wrote:
> digitig <digitig@gmail.com> writes:
>
> > When I run SPARK examiner (from within GPS) I Get the warning I'd like
> > to clear:
> >
> > warning: subprogram "Error_Header" has no effect.
>
> Try
>
> 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 => Off'").
I've found out how in older versions of SPARK I could annotate the procedure to say that it modified global outputs, but that depended on SPARK_Io, and the documentation on that says it has been replaced and I can't find either it or its replacement - the current SPARK documentation doesn't seem to mention either.
next prev parent reply other threads:[~2020-03-26 11:56 UTC|newest]
Thread overview: 9+ messages / expand[flat|nested] mbox.gz Atom feed top
2020-03-25 20:48 How do I resolve SPARK warning "procedure [...] has no effect for output procedure digitig
2020-03-25 23:38 ` Anh Vo
2020-03-26 0:45 ` digitig
2020-03-26 10:02 ` Simon Wright
2020-03-26 11:56 ` digitig [this message]
2020-03-26 13:13 ` Egil H H
2020-03-27 0:05 ` digitig
2020-03-26 15:36 ` Simon Wright
2020-03-26 12:04 ` Stephen Leake
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox