From: Stephen Leake <stephen_leake@stephe-leake.org>
Subject: Re: How do I resolve SPARK warning "procedure [...] has no effect for output procedure
Date: Thu, 26 Mar 2020 05:04:28 -0700 (PDT)
Date: 2020-03-26T05:04:28-07:00 [thread overview]
Message-ID: <a07fa9fd-0361-4dab-846b-826e64ce39a6@googlegroups.com> (raw)
In-Reply-To: <aa72dccb-e291-4849-ad37-9d001fad7234@googlegroups.com>
On Wednesday, March 25, 2020 at 1:48:44 PM UTC-7, digitig wrote:
> I'm trying to learn SPARK Ada, and, among other things, I have a procedure that simply puts a standard message to the screen. SPARK gives me a warning that the subprogram has no effect; I can see why - it only has the side-effect of printing to the screen. Everything I can see online to deal with this is a) *very* old, and b) uses SPARK_Io, which I understand is obsolete (and which I can't find). So what is the best way to tell SPARK that the procedure just has that side effect? (Hopefully better than `SPARK_mode => Off').
As far as SPARK is concerned, this procedure has no effect, so analyzing it is a waste of time. So you _should_ set SPARK_mode => Off for it; that is the right thing to do.
Why do you not want to do that?
-- Stephe
prev parent reply other threads:[~2020-03-26 12:04 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
2020-03-26 15:36 ` Simon Wright
2020-03-26 12:04 ` Stephen Leake [this message]
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox