From: Anh Vo <anhvofrcaus@gmail.com>
Subject: Re: How do I resolve SPARK warning "procedure [...] has no effect for output procedure
Date: Wed, 25 Mar 2020 16:38:04 -0700 (PDT)
Date: 2020-03-25T16:38:04-07:00 [thread overview]
Message-ID: <2cf70068-45e1-4e39-8ff4-3348f37e63fd@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'). >>>
Would you mind to post the source code and the warning message. So, every one is at the page.
next prev parent reply other threads:[~2020-03-25 23:38 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 [this message]
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
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox