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 17:05:19 -0700 (PDT)
Date: 2020-03-26T17:05:19-07:00 [thread overview]
Message-ID: <2358bc42-f67d-4af0-a686-97c1d2a547b8@googlegroups.com> (raw)
In-Reply-To: <1b1f6d93-b0ce-4fbf-82e4-272beb99fdde@googlegroups.com>
On Thursday, March 26, 2020 at 1:13:10 PM UTC, Egil H H wrote:
> On Thursday, March 26, 2020 at 12:56:04 PM UTC+1, digitig wrote:
> >
> > 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.
>
> In recent versions of GNAT, Ada.Text_IO includes SPARK aspects, like Global, so I guess that's the replacement for SPARK_IO you're looking for.
As simple as that! The thing I was looking for I had all along! Thanks, that's what I needed.
next prev parent reply other threads:[~2020-03-27 0:05 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
2020-03-26 13:13 ` Egil H H
2020-03-27 0:05 ` digitig [this message]
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