SPARK - precondition might fail (when there is no precondition)

SPARK - precondition might fail (when there is no precondition)

[Maciej Sobczak]

Hi,

Consider:

-- p.ads:
pragma SPARK_Mode;

package P is
   
   procedure Do_Nothing with No_Return;

end P;

-- p.adb:
pragma SPARK_Mode;

package body P is

   --pragma Warnings (Off);
   procedure Help_Doing_Nothing with No_Return;
   --pragma Warnings (On);
   
   procedure Help_Doing_Nothing is
   begin
      loop
         null;
      end loop;
   end Help_Doing_Nothing;

   --Dummy : Integer;
   procedure Do_Nothing is
   begin
      --Dummy := 0;
      Help_Doing_Nothing;
   end Do_Nothing;

end P;


There are two commented elements:
a) pragma Warnings Off/On around declaration of a helper procedure
b) Dummy integer variable with assignment that is there to look like an executable statement

If a) is commented, then GNATProve (20140405) complains that Help_Doing_Nothing has no effect.

If a) is uncommented but b) is commented, the error message says that Do_Nothing has no effect and there is no complaint about Help_Doing_Nothing.

If both a) and b) are uncommented, the error message says that precondition might fail in the line where Do_Nothing calls Help_Doing_Nothing.

All of these warnings can be seen with option --warnings=continue.

I sort of understand only the first message. The second case looks like SPARK is propagating the "has no effect" condition higher up the call chain.
The third case is a complete mystery to me - what precondition might fail there? I understand that it is a precondition for Help_Doing_Nothing, but it must be an implicit one and somehow the existence of variable D has an impact on it.
I have failed to locate the precondition check in the files generated by GNATProve.

Interestingly, the warning about precondition disappears when the aspect No_Return is removed from Do_Nothing, so it must be a factor here as well - but the SPARK RM does not describe any implicit preconditions related to subprograms used from No_Return-ing callers.

Any insight?

If you have access to a newer version of the tool, is there any difference?

-- 
Maciej Sobczak * http://www.inspirel.com