How do I resolve SPARK warning "procedure [...] has no effect for output procedure

How do I resolve SPARK warning "procedure [...] has no effect for output procedure

[digitig]

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').

Re: How do I resolve SPARK warning "procedure [...] has no effect for output procedure

[Anh Vo]

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.

Re: How do I resolve SPARK warning "procedure [...] has no effect for output procedure

[digitig]

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.

Re: How do I resolve SPARK warning "procedure [...] has no effect for output procedure

[Simon Wright]

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;

Re: How do I resolve SPARK warning "procedure [...] has no effect for output procedure

[digitig]

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.

Re: How do I resolve SPARK warning "procedure [...] has no effect for output procedure

[Egil H H]

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.

Re: How do I resolve SPARK warning "procedure [...] has no effect for output procedure

[digitig]

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.

Re: How do I resolve SPARK warning "procedure [...] has no effect for output procedure

[Simon Wright]

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.

Re: How do I resolve SPARK warning "procedure [...] has no effect for output procedure

[Stephen Leake]

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