From: Egil H H <ehh.public@gmail.com>
Subject: Re: How do I resolve SPARK warning "procedure [...] has no effect for output procedure
Date: Thu, 26 Mar 2020 06:13:08 -0700 (PDT)
Date: 2020-03-26T06:13:08-07:00 [thread overview]
Message-ID: <1b1f6d93-b0ce-4fbf-82e4-272beb99fdde@googlegroups.com> (raw)
In-Reply-To: <a552d00c-39f2-4dc7-85b8-4b663405e363@googlegroups.com>
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.
next prev parent reply other threads:[~2020-03-26 13:13 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 [this message]
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