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

[digitig <digitig@gmail.com>]

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.