Re: Hide annotations on procedures.

[Phil Thornley <phil.jpthornley@googlemail.com>]

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