* How do I resolve SPARK warning "procedure [...] has no effect for output procedure
@ 2020-03-25 20:48 digitig
2020-03-25 23:38 ` Anh Vo
2020-03-26 12:04 ` Stephen Leake
0 siblings, 2 replies; 9+ messages in thread
From: digitig @ 2020-03-25 20:48 UTC (permalink / raw)
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').
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: How do I resolve SPARK warning "procedure [...] has no effect for output procedure
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 12:04 ` Stephen Leake
1 sibling, 1 reply; 9+ messages in thread
From: Anh Vo @ 2020-03-25 23:38 UTC (permalink / raw)
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.
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: How do I resolve SPARK warning "procedure [...] has no effect for output procedure
2020-03-25 23:38 ` Anh Vo
@ 2020-03-26 0:45 ` digitig
2020-03-26 10:02 ` Simon Wright
0 siblings, 1 reply; 9+ messages in thread
From: digitig @ 2020-03-26 0:45 UTC (permalink / raw)
On Wednesday, March 25, 2020 at 11:38:06 PM UTC, Anh Vo wrote:
> Would you mind to post the source code and the warning message. So, every one is at the page.
Ok, here's a simplified thing that gives the same issue:
Suppose I've got a naive error logging procedure (to isolate the use of Standard_Error, which Spark doesn't like and I don't know how to get at the underlying file in Ada yet):
with Ada.Text_IO; use Ada.Text_IO;
package body Logging is
procedure Log_Error(Message: String) with SPARK_Mode => Off is
begin
Put_Line(Standard_Error, Message);
end Log_Error;
end Logging;
As you can see, SPARK is turned off for that. Then I have (simplified) :
with Logging; use Logging;
with Ada.Characters.Latin_1; use Ada.Characters.Latin_1;
package body Utils is
procedure Error_Header is
begin
Log_Error
("This is the standard header I want for the Standard_Error output" &
LF);
end Error_Header;
end Utils;
When I run SPARK examiner (from within GPS) I Get the warning I'd like to clear:
warning: subprogram "Error_Header" has no effect.
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: How do I resolve SPARK warning "procedure [...] has no effect for output procedure
2020-03-26 0:45 ` digitig
@ 2020-03-26 10:02 ` Simon Wright
2020-03-26 11:56 ` digitig
0 siblings, 1 reply; 9+ messages in thread
From: Simon Wright @ 2020-03-26 10:02 UTC (permalink / raw)
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;
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: How do I resolve SPARK warning "procedure [...] has no effect for output procedure
2020-03-26 10:02 ` Simon Wright
@ 2020-03-26 11:56 ` digitig
2020-03-26 13:13 ` Egil H H
2020-03-26 15:36 ` Simon Wright
0 siblings, 2 replies; 9+ messages in thread
From: digitig @ 2020-03-26 11:56 UTC (permalink / raw)
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.
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: How do I resolve SPARK warning "procedure [...] has no effect for output procedure
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 12:04 ` Stephen Leake
1 sibling, 0 replies; 9+ messages in thread
From: Stephen Leake @ 2020-03-26 12:04 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: How do I resolve SPARK warning "procedure [...] has no effect for output procedure
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
1 sibling, 1 reply; 9+ messages in thread
From: Egil H H @ 2020-03-26 13:13 UTC (permalink / raw)
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.
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: How do I resolve SPARK warning "procedure [...] has no effect for output procedure
2020-03-26 11:56 ` digitig
2020-03-26 13:13 ` Egil H H
@ 2020-03-26 15:36 ` Simon Wright
1 sibling, 0 replies; 9+ messages in thread
From: Simon Wright @ 2020-03-26 15:36 UTC (permalink / raw)
digitig <digitig@gmail.com> writes:
> I specifically said I wanted to resolve it, not hide it ("Hopefully
> better than `SPARK_mode => Off'").
It's not that uncommon in SPARK to have to annotate to explain why
some apparent problem is not in fact so.
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: How do I resolve SPARK warning "procedure [...] has no effect for output procedure
2020-03-26 13:13 ` Egil H H
@ 2020-03-27 0:05 ` digitig
0 siblings, 0 replies; 9+ messages in thread
From: digitig @ 2020-03-27 0:05 UTC (permalink / raw)
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.
^ permalink raw reply [flat|nested] 9+ messages in thread
end of thread, other threads:[~2020-03-27 0:05 UTC | newest]
Thread overview: 9+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
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 is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox