Hide annotations on procedures.

Hide annotations on procedures.

[xorque]

Having failed to take the day off from learning SPARK, I've run into
a strange problem regarding procedure annotations.

I have the following in a package body:

  procedure C_Readlink_Boundary
    (File_Name     : in String;
     Buffer        : out String;
     Buffer_Size   : in File.File_Name_Index_t;
     Returned_Size : out C_Types.Signed_Size_t)
  is
    --# hide C_Readlink_Boundary
  begin
    null;
  end C_Readlink_Boundary;

The body of the procedure is obviously not implemented yet. The
procedure
itself is defined only in the body of the package, not accessible from
outside.
The body of the procedure is intended to be hidden from SPARK. The
problem
I have is that SPARK doesn't seem to get it:

   7    procedure C_Readlink_Boundary
                  ^
***        Semantic Error    :154: The subprogram or task body
C_Readlink_Boundary
           does not have an annotation.

The procedure doesn't touch any global variables. Any 'derives'
annotation added to the procedure is rejected by SPARK (as it would
need to
go on the procedure specification - which doesn't exist). I've used
the same
pattern on functions, not procedures, and SPARK has accepted it.

What have I done wrong here?

Re: Hide annotations on procedures.

[Phil Thornley]

On 12 June, 14:35, xorque <xorquew...@googlemail.com> wrote:
> Having failed to take the day off from learning SPARK, I've run into
> a strange problem regarding procedure annotations.
>
> I have the following in a package body:
>
>   procedure C_Readlink_Boundary
>     (File_Name     : in String;
>      Buffer        : out String;
>      Buffer_Size   : in File.File_Name_Index_t;
>      Returned_Size : out C_Types.Signed_Size_t)
>   is
>     --# hide C_Readlink_Boundary
>   begin
>     null;
>   end C_Readlink_Boundary;
>
> The body of the procedure is obviously not implemented yet. The
> procedure
> itself is defined only in the body of the package, not accessible from
> outside.
> The body of the procedure is intended to be hidden from SPARK. The
> problem
> I have is that SPARK doesn't seem to get it:
>
>    7    procedure C_Readlink_Boundary
>                   ^
> ***        Semantic Error    :154: The subprogram or task body
> C_Readlink_Boundary
>            does not have an annotation.
>
> The procedure doesn't touch any global variables. Any 'derives'
> annotation added to the procedure is rejected by SPARK (as it would
> need to
> go on the procedure specification - which doesn't exist). I've used
> the same
> pattern on functions, not procedures, and SPARK has accepted it.
>
> What have I done wrong here?

The derives annotation is certainly needed and goes immediately after
the procedure declaration - before the 'is'. (The hide goes after the
'is'.)

Are you getting it in the wrong position, or making some other error
in that annotation?

Phil Thornley

Re: Hide annotations on procedures.

[xorque]

Phil Thornley wrote:
> The derives annotation is certainly needed and goes immediately after
> the procedure declaration - before the 'is'. (The hide goes after the
> 'is'.)

Argh!

I was putting it after the 'is'.

Nice catch...